6 files changed, 62 insertions, 16 deletions
diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js
new file mode 100644
index 0000000000..371c5adc00
--- /dev/null
+++ b/dev/Coq_Bugzilla_autolink.user.js
@@ -0,0 +1,34 @@
+// ==UserScript==
+// @name        Coq Bugzilla autolink
+// @namespace   SkySkimmer
+// @include     https://github.com/coq/coq/*
+// @description Makes BZ#XXXX into links to bugzilla for GitHub
+// @version     1
+// @grant       none
+// ==/UserScript==
+
+var regex = /BZ#(\d+)/g;
+var substr = '<a href="https://coq.inria.fr/bugs/show_bug.cgi?id=$1">$&</a>';
+
+function doNode(node)
+{
+    node.innerHTML = node.innerHTML.replace(regex,substr);
+}
+
+var comments = document.getElementsByClassName("comment-body");
+
+for(var i=0; i<comments.length; i++)
+{
+    var pars = comments[i].getElementsByTagName("p");
+    for(var j=0; j<pars.length; j++)
+    {
+        doNode(pars[j]);
+    }
+}
+
+// usually 1 or 0 titles...
+var titles = document.getElementsByClassName("js-issue-title");
+for(var i=0; i<titles.length; i++)
+{
+    doNode(titles[i]);
+}
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index a420b5d8bb..f91b301b8c 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -328,12 +328,6 @@ ECHO ========== INSTALL CYGWIN ==========
 REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
 REM Otherwise chmod won't work and e.g. the ocaml build will fail.
 REM Cygwin setup does not touch the ACLs of existing folders.
-REM => Create the setup log in a temporary location and move it later.
-
-REM Get Unique temporary file name
-:logfileloop
-SET LOGFILE=%TEMP%\CygwinSetUp%RANDOM%-%RANDOM%-%RANDOM%-%RANDOM%.log
-if exist "%LOGFILE%" GOTO logfileloop
 
 REM Run Cygwin Setup
 
@@ -348,6 +342,12 @@ IF "%COQREGTESTING%" == "Y" (
   SET RUNSETUP=Y
 )
 
+SET "EXTRAPACKAGES= "
+
+IF NOT "%APPVEYOR%" == "True" (
+  SET EXTRAPACKAGES="-P wget,curl,git,gcc-core,gcc-g++,automake1.5"
+)
+
 IF "%RUNSETUP%"=="Y" (
   %SETUP% ^
     --proxy "%PROXY%" ^
@@ -356,10 +356,9 @@ IF "%RUNSETUP%"=="Y" (
     --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
     --no-shortcuts ^
     %CYGWIN_OPT% ^
-    -P wget,curl,git,make,unzip ^
-    -P gcc-core,gcc-g++ ^
+    -P make,unzip ^
     -P gdb,liblzma5 ^
-    -P patch,automake1.14,automake1.15 ^
+    -P patch,automake1.14 ^
     -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
     -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
     -P libiconv-devel,libunistring-devel,libncurses-devel ^
@@ -369,12 +368,11 @@ IF "%RUNSETUP%"=="Y" (
     -P gtk-update-icon-cache ^
     -P libtool,automake ^
     -P intltool ^
-    > "%LOGFILE%" ^
+    %EXTRAPACKAGES% ^
     || GOTO ErrorExit
 
   MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
   MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
-  MOVE  "%LOGFILE%" "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log" || GOTO ErrorExit
 )
 
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index f3e4cec0b9..f12cbe0a78 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -910,6 +910,10 @@ function make_camlp5 {
     log2 make install
     # For some reason gramlib.a is not copied, but it is required by Coq
     cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/"
+    # For some reason META is not copied, but it is required by coq_makefile
+    log2 make -C etc META
+    mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/"
+    cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/"
     log2 make clean
     build_post
   fi
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index ca6a5643c1..e2fbf1f6d1 100644
--- a/dev/ci/appveyor.bat
+++ b/dev/ci/appveyor.bat
@@ -23,13 +23,19 @@ if %USEOPAM% == false (
   call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
     -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
     -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-    -setup %CYGROOT%\%SETUP%
-  copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis
-  7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\*
+    -setup %CYGROOT%\%SETUP% || GOTO ErrorExit
+  copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
+  7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
 )
 
 if %USEOPAM% == true (
   %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
     -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
-  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh
+  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit
 )
+
+GOTO :EOF
+
+:ErrorExit
+  ECHO ERROR MakeCoq_MinGW.bat failed
+  EXIT /b 1
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 358f527f9e..1bfdf7dfbe 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -5,6 +5,7 @@ set -xe
 if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN=`pwd`/_install_ci/bin
+    export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME"
 else
     export COQBIN=`pwd`/bin
 fi
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 127b4a6d2d..cf7d205d8b 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -291,7 +291,10 @@ Pseudocode for listing all of the goals in order: `rev (flat_map fst background)
 
 
 ### <a name="command-status">**Status(force: bool)**</a>
-CoqIDE typically sets `force` to `false`. 
+Returns information about the current proofs. CoqIDE typically sends this
+message with `force = false` after each sentence, and with `force = true` if
+the user wants to force the checking of all proofs (wheels button). In terms of
+the STM API, `force` triggers a `Join`.
 ```html
 <call val="Status"><bool val="${force}"/></call>
 ```