aboutsummaryrefslogtreecommitdiff
path: root/dev/db
diff options
context:
space:
mode:
authorPierre Courtieu2014-12-16 14:13:59 +0100
committerPierre Courtieu2014-12-16 14:13:59 +0100
commit5ba84979df97996cd04f44e506742bb58ecf0465 (patch)
tree565c966fd3f4f73a2182337933e147d73a4c6971 /dev/db
parentc816bdb44625b6dba8efa4b0ba39f162b06b737d (diff)
msg_info now puts infomsg tag in emacs mode.
Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal.
Diffstat (limited to 'dev/db')
0 files changed, 0 insertions, 0 deletions