diff options
Diffstat (limited to 'build/mkmyocamlbuild_config.sh')
-rwxr-xr-x | build/mkmyocamlbuild_config.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/build/mkmyocamlbuild_config.sh b/build/mkmyocamlbuild_config.sh index e48f5b0e0b..9c7eebd3c3 100755 --- a/build/mkmyocamlbuild_config.sh +++ b/build/mkmyocamlbuild_config.sh @@ -19,6 +19,7 @@ cd `dirname $0`/.. sed \ -e 's/^.*FLEXDIR.*$//g' \ -e 's/^#ml \(.*\)/\1/' \ + -e 's/^\([^"][^"]*\("[^"]*"[^"]*\)*\)#.*$/\1/' \ -e 's/^\(#.*\)$/(* \1 *)/' \ -e 's/^\(.*\$([0-9]).*\)$/(* \1 *)/' \ -e 's/^\([^(=]*\)=\([^"]*\)$/let <:lower<\1>> = "\2";;/' \ |