aboutsummaryrefslogtreecommitdiff
path: root/dev/build/windows
diff options
context:
space:
mode:
authorMichael Soegtrop2019-05-09 21:24:22 +0200
committerMichael Soegtrop2019-05-09 21:24:22 +0200
commit8ee7a4a7003fc2c5b01e0d6041961b3da14c0c84 (patch)
tree091cc0f363ce7f43d85a490c895c1ea5e5f69226 /dev/build/windows
parent474507d70f967358d993465cf7fc2a9a5e1bbd29 (diff)
parent053e64206aa70c6a12c75b59e8267eeaba00d1ce (diff)
Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repo
Reviewed-by: MSoegtropIMC
Diffstat (limited to 'dev/build/windows')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh13
1 files changed, 0 insertions, 13 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index ea9af60330..d737632638 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1630,19 +1630,6 @@ function make_addon_ssreflect {
fi
}
-# Ltac-2 plugin
-# A new (experimental) tactic language
-
-function make_addon_ltac2 {
- installer_addon_dependency ltac2
- if build_prep_overlay ltac2; then
- installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" ""
- log1 make $MAKE_OPT all
- log2 make install
- build_post
- fi
-}
-
# UniCoq plugin
# An alternative unification algorithm
function make_addon_unicoq {