diff options
Diffstat (limited to 'source/l/mpfr/patches.url')
| -rw-r--r-- | source/l/mpfr/patches.url | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/source/l/mpfr/patches.url b/source/l/mpfr/patches.url new file mode 100644 index 000000000..b477cd613 --- /dev/null +++ b/source/l/mpfr/patches.url @@ -0,0 +1,2 @@ +# Fetched like this: +https://www.mpfr.org/mpfr-current/patch01 |