aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-23 21:36:49 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-23 21:36:49 +0100
commit67f7e1103ffb5dae052595e4db00e0214e54474d (patch)
tree589f413f7cfcc3f627201bd0fcb8ba553c10d20e /test-suite/output
parent62ce0d1ec197d70a81faf12e151a3da618b2d1ba (diff)
parent8c42932d1788c8924844d8fa22419f6fb4401030 (diff)
Merge PR#503: make check not CoqIDE-specific
Diffstat (limited to 'test-suite/output')
0 files changed, 0 insertions, 0 deletions