aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2019-02-16 15:14:46 +0100
committerGaëtan Gilbert2019-02-18 21:24:11 +0100
commitea8a9125a4e81e7c848cf53f1e34f534d359e832 (patch)
tree3495980fb3efcc41fd2cd658ac3ead6b12f47846 /plugins/syntax/string_notation.ml
parent2e4e082637771bc047fbd977aaa5de26956c4618 (diff)
[sphinx] Add abort and restart options to directive coqtop.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions