diff options
Diffstat (limited to 'build')
| -rwxr-xr-x | build/mkmyocamlbuild_config.sh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/build/mkmyocamlbuild_config.sh b/build/mkmyocamlbuild_config.sh index 397a2997bd..ef86ab7421 100755 --- a/build/mkmyocamlbuild_config.sh +++ b/build/mkmyocamlbuild_config.sh @@ -14,4 +14,7 @@ sed \ -e 's/^let <lower>\(MAKE\|DO\).*$//g' \ -e 's/"true"/true/g' \ -e 's/"false"/false/g' \ - config/Makefile | sed -f build/tolower.sed | sed -f build/tolower.sed > myocamlbuild_config.ml + config/Makefile | \ + sed -f build/tolower.sed | \ + sed -f build/tolower.sed | \ + sed -f build/tolower.sed > myocamlbuild_config.ml |