From ce22501ca90e3c6e7124de4eeb4ad3c0a2615666 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Dec 2017 21:04:22 +0100
Subject: Gitlab: don't ./configure in documentation job

The config/Makefile is carried over by artefacts.
---
 .gitlab-ci.yml | 1 -
 1 file changed, 1 deletion(-)

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"
-- 
cgit v1.2.3