From 360fafb7781ca12e533f7ee55da6a4a4324e2a19 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 17 Nov 2018 02:48:09 +0100
Subject: [ci] Uniformize casing of makefile targets and ci variables.

This is convenient as to have better automation.
---
 Makefile.ci | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Makefile.ci')

diff --git a/Makefile.ci b/Makefile.ci
index e8fea11bdb..88ea64974a 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -9,12 +9,12 @@
 ##########################################################################
 
 CI_TARGETS= \
-    ci-aac-tactics \
+    ci-aac_tactics \
     ci-bedrock2 \
     ci-bignums \
     ci-color \
     ci-compcert \
-    ci-coq-dpdgraph \
+    ci-coq_dpdgraph \
     ci-coquelicot \
     ci-corn \
     ci-cpdt \
@@ -38,7 +38,7 @@ CI_TARGETS= \
     ci-mtac2 \
     ci-paramcoq \
     ci-pidetop \
-    ci-plugin-tutorial \
+    ci-plugin_tutorial \
     ci-quickchick \
     ci-sf \
     ci-simple-io \
-- 
cgit v1.2.3