From 2434e85e1f2006e66efd74bd6cd7224e301e3bff Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 8 Dec 2017 10:50:09 +0100
Subject: Fix a copy-paste error in ci-ltac2.

---
 dev/ci/ci-ltac2.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
index 4865be31ec..ed40036012 100755
--- a/dev/ci/ci-ltac2.sh
+++ b/dev/ci/ci-ltac2.sh
@@ -3,7 +3,7 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
+ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2
 
 git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR}
 
-- 
cgit v1.2.3