aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/xml_parser.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-16 16:57:59 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-16 17:34:57 +0200
commit4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (patch)
tree2987141c16e3ec03afc1d3b11cb3d7b3334c6580 /lib/xml_parser.ml
parent26aa224293e88611dcb543e400488013bc8b30b4 (diff)
Undo prints only if coqtop || emacs
Diffstat (limited to 'lib/xml_parser.ml')
0 files changed, 0 insertions, 0 deletions