aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_syntax_plugin.mlpack
diff options
context:
space:
mode:
authorThéo Zimmermann2018-05-22 19:00:40 +0200
committerThéo Zimmermann2018-06-05 14:41:54 +0200
commit22b4d8c5b410e82f4bd1a78947d26e9dd4a3a6e3 (patch)
treef26806eab04a6a33e7238803e071ef77099010a5 /plugins/syntax/string_syntax_plugin.mlpack
parent2ee47cd259a912196b9e4a03412f5d786380d29c (diff)
Workaround a weird error of .. coqtop::
Diffstat (limited to 'plugins/syntax/string_syntax_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions