aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-06-13 17:09:47 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-06-13 17:09:47 +0200
commitab1f43defa72e93617c3e3b09abb1876ff5a1b46 (patch)
tree0531751e83ad6b4ee30971b63c1a1d0c7a8429fe /library/library.ml
parentf6781defd922b80f8c48c4798c29644c99d5e611 (diff)
STM classification: VernacTimeout may contain an "internal command".
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions