diff options
| -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 '}' |