aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-ltac2.sh
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci/ci-ltac2.sh')
-rwxr-xr-xdev/ci/ci-ltac2.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
index 4865be31e..ed4003601 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}