From d21c7aca1d1ce94e2007f0e6c550d36230d9f64f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 8 Oct 2018 15:39:31 +0200
Subject: [ci] Add aac-tactics.

And fix a typo that was previously there.
---
 .gitlab-ci.yml                     | 3 +++
 Makefile.ci                        | 4 +++-
 dev/build/windows/makecoq_mingw.sh | 2 +-
 dev/ci/ci-aac-tactics.sh           | 8 ++++++++
 dev/ci/ci-basic-overlay.sh         | 6 +++---
 5 files changed, 18 insertions(+), 5 deletions(-)
 create mode 100755 dev/ci/ci-aac-tactics.sh

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 18f515da24..6aa2cecbd3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -346,6 +346,9 @@ validate:edge+flambda:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
 
+ci-aac-tactics:
+  <<: *ci-template
+
 ci-bedrock2:
   <<: *ci-template
 
diff --git a/Makefile.ci b/Makefile.ci
index fb4f275e9e..8234da0869 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -8,7 +8,9 @@
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
 
-CI_TARGETS=ci-bedrock2 \
+CI_TARGETS= \
+    ci-aac-tactics \
+    ci-bedrock2 \
     ci-bignums \
     ci-color \
     ci-compcert \
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index b8bea755e0..c3d895784e 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1851,7 +1851,7 @@ function make_addon_coquelicot {
 
 function make_addon_aactactics {
   installer_addon_dependency aac
-  if build_prep_overlay aactactis; then
+  if build_prep_overlay aactactics; then
     installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" ""
     log1 make
     log2 make install
diff --git a/dev/ci/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh
new file mode 100755
index 0000000000..896a0ddf66
--- /dev/null
+++ b/dev/ci/ci-aac-tactics.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download aactactics
+
+( cd "${CI_BUILD_DIR}/aactactics" && make && make install )
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 511eaaba9c..50d4d21637 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -252,6 +252,6 @@
 ########################################################################
 # aac-tactics
 ########################################################################
-: "${aactactis_CI_REF:=master}"
-: "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
-: "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}"
+: "${aactactics_CI_REF:=master}"
+: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
+: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}"
-- 
cgit v1.2.3