aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-29 14:15:06 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-29 17:25:23 +0200
commite581d018bfeaec2ffdf8697950eede5ce4282716 (patch)
tree6e3e43d5f8909ab2b7085cbacdf32a1b64a94007 /Makefile.common
parent799d17738ebbae30a007b308998a669a9139cf1d (diff)
Avoid running interactive tests on Windows.
This is a temporary workaround, until we fix the underlying issue which makes coqtop hang on those tests.
Diffstat (limited to 'Makefile.common')
0 files changed, 0 insertions, 0 deletions