aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ide
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-21 17:14:29 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-21 17:14:29 +0200
commitc0fdb912c5e63bb43d6e8dd320e9f5613c6237ff (patch)
treeab0e7f43c58a2554f78f317893eb69120dae5dd4 /Makefile.ide
parentf30269579b78d5bf65dcd5db70e341fe9598b274 (diff)
parent5b3d0f2cd7a5f480fe24a938e2f6713798c7139a (diff)
Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)
Diffstat (limited to 'Makefile.ide')
0 files changed, 0 insertions, 0 deletions