aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/aux_file.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-03-12 11:51:21 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-03-12 11:51:21 +0100
commita622c4c951f559fa05d45a45b4b25ace00793281 (patch)
tree6374524264f598772affbf2f22ac5feed4b2c8a8 /lib/aux_file.mli
parent1142dab2ee08b23cdf97cdf52d5dc7ecd7768967 (diff)
CoqIDE: Errors page gets red if not empty
Diffstat (limited to 'lib/aux_file.mli')
0 files changed, 0 insertions, 0 deletions