diff options
author | 2017-12-22 16:01:25 +0100 | |
---|---|---|
committer | 2017-12-22 16:01:25 +0100 | |
commit | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (patch) | |
tree | f54c7bffd448f39538187aefedd641698805153f | |
parent | ff5d440a8158c1ae46604c9557b495e3f45eb077 (diff) | |
parent | ce22501ca90e3c6e7124de4eeb4ad3c0a2615666 (diff) |
Merge PR #6465: Gitlab touchup
-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 e56693eac..6b52870ce 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" |