Merge PR coq#9470: the default branch of Mtac2 changed to master

Reviewed-by: ejgallego
ggonthier · Feb 4, 2019 · 5c1d7fc · 5c1d7fc
2 parents f177aa5 + 402458b
commit 5c1d7fc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
@@ -35,7 +35,7 @@
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
 : "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
 
-: "${mtac2_CI_REF:=master-sync}"
+: "${mtac2_CI_REF:=master}"
 : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}"
 : "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}"