diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-21 08:36:27 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-05 17:12:00 +0200 |
| commit | ccf33e7aed7f6c8cdfa6ec6ebb6b5f094ed6989f (patch) | |
| tree | 551337948da42b5de35a2cf3c4da5845ab503aff | |
| parent | 8ac880bee5611a0a408158ff021277c6157eccce (diff) | |
Adapt Windows build script to new CoqIDE data installation directory.
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 9507fe79b..5352b1dce 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1058,13 +1058,18 @@ function copq_coq_gtk { install_rec "$PREFIX/share/themes/" '*' "$PREFIXCOQ/share/themes" # This below item look like a bug in make install + if [ -d "$PREFIXCOQ/share/coq/" ] ; then + COQSHARE="$PREFIXCOQ/share/coq/" + else + COQSHARE="$PREFIXCOQ/share/" + fi if [[ ! $COQ_VERSION == 8.4* ]] ; then - mv "$PREFIXCOQ/share/coq/"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" - mv "$PREFIXCOQ/share/coq/"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles" + mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" + mv "$COQSHARE"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles" fi mkdir -p "$PREFIXCOQ/ide" - mv "$PREFIXCOQ/share/coq/"*.png "$PREFIXCOQ/ide" - rmdir "$PREFIXCOQ/share/coq" + mv "$COQSHARE"*.png "$PREFIXCOQ/ide" + rmdir "$PREFIXCOQ/share/coq" || true fi } |