diff options
-rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -1,6 +1,6 @@ #! /bin/sh -if [ sed --version >/dev/null 2>&1 ]; then +if sed --version >/dev/null 2>&1; then GSED=sed else GSED=gsed |
index : mulk/mulklib | ||
Functional utilities and persistent data structures for C. | Matthias Benkard |
aboutsummaryrefslogtreecommitdiff |
-rwxr-xr-x | configure | 2 |
@@ -1,6 +1,6 @@ #! /bin/sh -if [ sed --version >/dev/null 2>&1 ]; then +if sed --version >/dev/null 2>&1; then GSED=sed else GSED=gsed |