diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -1008,6 +1008,7 @@ fi ############################################## mlconfig_file="$COQSRC/config/coq_config.ml" +mymlconfig_file="$COQSRC/myocamlbuild_config.ml" config_file="$COQSRC/config/Makefile" config_template="$COQSRC/config/Makefile.template" @@ -1065,7 +1066,7 @@ esac # Building the $COQTOP/config/coq_config.ml file ##################################################### -rm -f "$mlconfig_file" +rm -f "$mlconfig_file" "$mymlconfig_file" cat << END_OF_COQ_CONFIG > $mlconfig_file (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) @@ -1132,7 +1133,7 @@ subdirs plugins echo "]" >> "$mlconfig_file" chmod a-w "$mlconfig_file" - +ln -sf "$mlconfig_file" "$mymlconfig_file" ############################################### # Building the $COQTOP/config/Makefile file |