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 2349000e5..a6ccecbca 100755
--- a/configure
+++ b/configure
@@ -795,10 +795,15 @@ case $libdir_spec in
*) LIBDIR_OPTION="None";;
esac
-case $configdir_spec/$local in
- yes/*) CONFIGDIR=$configdir;;
- */true) CONFIGDIR=$COQTOP/ide
- configdir_spec=yes;;
+case $configdir_spec/$prefix_spec/$local in
+ yes/*/*) CONFIGDIR=$configdir;;
+ */yes/*) configdir_spec=yes
+ case $ARCH in
+ win32) CONFIGDIR=$prefix/config;;
+ *) CONFIGDIR=$prefix/etc/xdg/coq;;
+ esac;;
+ */*/true) CONFIGDIR=$COQTOP/ide
+ configdir_spec=yes;;
*) printf "Where should I install the Coqide configuration files [$configdir_def]? "
read CONFIGDIR
case $CONFIGDIR in