aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-01-15 13:54:01 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-01-15 14:18:49 +0100
commit1856d60057ac9096c791d71d4282c0cdfef85913 (patch)
treef8b33554b85c09ce9792eca55a7e74bf6f3d7362 /configure.ml
parent54083a2a8e6c4c2083717ac18c7b4dc351ab0f7d (diff)
More tests on brackets with goal selectors (including failures).
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions