diff options
author | vlefevre <vlefevre@280ebfd0-de03-0410-8827-d642c229c3f4> | 2019-08-02 08:22:52 +0000 |
---|---|---|
committer | vlefevre <vlefevre@280ebfd0-de03-0410-8827-d642c229c3f4> | 2019-08-02 08:22:52 +0000 |
commit | f034940f3afae7f065f524ff8fb57aefe68772d1 (patch) | |
tree | aa303a1f9a79b52354beef25d65d7b40f3d9b196 /tools | |
parent | 15956538dcafb5957499c1bf2258e75cfbce148c (diff) | |
download | mpfr-f034940f3afae7f065f524ff8fb57aefe68772d1.tar.gz |
[tools/get_patches.sh] Fixed change in r13543 (the contents of PATCHES
should still be written as a list of words separated by a space).
git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/trunk@13544 280ebfd0-de03-0410-8827-d642c229c3f4
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/get_patches.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/get_patches.sh b/tools/get_patches.sh index 5d93c3926..5b75a0df0 100755 --- a/tools/get_patches.sh +++ b/tools/get_patches.sh @@ -39,5 +39,6 @@ mpfr_get_patches (void) { EOF -echo " return \"$patches\";" +# $patches is written as a list of words separated by a space character. +echo ' return "'$patches'";' echo '}' |