diff options
Diffstat (limited to 'mpi-patches/series')
| -rw-r--r-- | mpi-patches/series | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/mpi-patches/series b/mpi-patches/series new file mode 100644 index 00000000..71aa73ba --- /dev/null +++ b/mpi-patches/series @@ -0,0 +1,8 @@ +config-types +fix-warnings +use-txr-allocator +add-mp-set-intptr +export-mp-eq +add-mp-hash +add-mpi-toradix-with-case +fix-mult-bug |