diff options
| author | Maxime Dénès | 2015-07-02 16:16:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-07-02 16:16:46 +0200 |
| commit | 27de0f2d7e5cd0cc4b221413dfe3c7b739104350 (patch) | |
| tree | a42625106f71295ebc2011b797603cd1b3b8ec83 /dev | |
| parent | a28d9981e5baf812de14e62de8d904e545e804e5 (diff) | |
| parent | 44f45f58dc0a169286c9fcfa7d2edbc8bc04673b (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/make-installer-win32.sh | 2 | ||||
| -rwxr-xr-x | dev/make-installer-win64.sh | 4 | ||||
| -rw-r--r-- | dev/printers.mllib | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh index ec7cd5773a..c6ed2f401d 100755 --- a/dev/make-installer-win32.sh +++ b/dev/make-installer-win32.sh @@ -5,7 +5,7 @@ ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download -[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no +[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no make -j2 if [ ! -e bin/make.exe ]; then wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh index 73e1fdbeb2..03fdda4aa1 100755 --- a/dev/make-installer-win64.sh +++ b/dev/make-installer-win64.sh @@ -5,13 +5,13 @@ ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download -[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no +[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no make -j2 coqide mkdir -p bin32 cp bin/* bin32/ make clean make archclean -( . ${BASE}_64/environ; ./configure -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs ) +( . ${BASE}_64/environ; ./configure -debug -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs ) cp bin32/coqide* bin/ if [ ! -e bin/make.exe ]; then wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" diff --git a/dev/printers.mllib b/dev/printers.mllib index 74f36f6f5a..07b48ed573 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -110,7 +110,6 @@ Loadpath Goptions Decls Heads -Assumptions Keys Locusops Miscops @@ -204,6 +203,7 @@ Hints Himsg Cerrors Locality +Assumptions Vernacinterp Dischargedhypsmap Discharge |