aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/gitlab.bat
diff options
context:
space:
mode:
authorGravatar Michael Soegtrop <michael.soegtrop@intel.com>2018-06-15 18:57:00 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-25 16:37:02 +0200
commitcb885e8c70a75043ff89e117c29cbb5dc22ff16f (patch)
tree9b9d84ef9f0b7151c33bb889493679e01aad92d6 /dev/ci/gitlab.bat
parent915452f9a73d25e45131edb08531c29a79ab7020 (diff)
Fix for issue 7707: include Ltac2 and Equations in Windows build
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
Diffstat (limited to 'dev/ci/gitlab.bat')
0 files changed, 0 insertions, 0 deletions