diff options
| author | Gaëtan Gilbert | 2017-12-18 21:04:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-18 21:04:22 +0100 |
| commit | ce22501ca90e3c6e7124de4eeb4ad3c0a2615666 (patch) | |
| tree | 106ff9673f79dcb2b034b62af1a39b6317b1f113 | |
| parent | 80158e796b6df8eb36117f349c312127c5729a8c (diff) | |
Gitlab: don't ./configure in documentation job
The config/Makefile is carried over by artefacts.
| -rw-r--r-- | .gitlab-ci.yml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e56693eac2..6b52870ce6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -136,7 +136,6 @@ before_script: stage: test script: - INSTALLDIR=$(readlink -f _install_ci) - - ./configure -prefix "$INSTALLDIR" ${EXTRA_CONF} - cp "$INSTALLDIR/lib/coq/tools/coqdoc/coqdoc.sty" . - LIB="$INSTALLDIR/lib/coq" |