aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/float_syntax.ml
diff options
context:
space:
mode:
authorHugo Herbelin2020-01-19 08:43:36 +0100
committerGitHub2020-01-19 08:43:36 +0100
commit927c683116c17a4746afdc4000ba2015591d3ba2 (patch)
treeb4f88427caf935b211a2154fc6a1c7436c798e0c /plugins/syntax/float_syntax.ml
parent1f3ad4f8ebbf48d68488d19335d3c2db18e248f4 (diff)
Removing text saying XML is future of PG, adding explicitly vscoq as a user
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions