aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure
diff options
context:
space:
mode:
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure13
1 files changed, 9 insertions, 4 deletions
diff --git a/configure b/configure
index 8e49f3738..0ca4c98ba 100755
--- a/configure
+++ b/configure
@@ -27,6 +27,7 @@ coq_debug_flag=
coq_profile_flag=
byte_opt_tools=opt
+local=false
bindir_spec=no
libdir_spec=no
mandir_spec=no
@@ -49,8 +50,9 @@ while : ; do
mandir_spec=yes
mandir=$2/man
shift;;
- -local|--local) bindir_spec=yes
- bindir=$COQTOP/bin/${arch-`arch`}
+ -local|--local) local=true
+ bindir_spec=yes
+ bindir=$COQTOP
libdir_spec=yes
libdir=$COQTOP
mandir_spec=yes
@@ -365,7 +367,8 @@ rm -f $COQTOP/config/Makefile
case $ARCH in
win32)
- sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
+ sed -e "s|LOCALINSTALLATION|$local|" \
+ -e "s|COQTOPDIRECTORY|$COQTOP|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|`echo $BINDIR |sed -e 's|\\\|/|g'`|" \
-e "s|COQLIBDIRECTORY|`echo $LIBDIR |sed -e 's|\\\|/|g'`|" \
@@ -389,7 +392,8 @@ case $ARCH in
-e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
$COQTOP/config/Makefile.template > $COQTOP/config/Makefile;;
*)
- sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
+ sed -e "s|LOCALINSTALLATION|$local|" \
+ -e "s|COQTOPDIRECTORY|$COQTOP|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|$BINDIR|" \
-e "s|COQLIBDIRECTORY|$LIBDIR|" \
@@ -423,6 +427,7 @@ rm -f $mlconfig_file
cat << END_OF_COQ_CONFIG > $mlconfig_file
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
+let local = $local
let bindir = "$BINDIR"
let coqlib = "$LIBDIR"
let coqtop = "$COQTOP"