aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/envars.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-24 08:23:36 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-24 08:26:24 +0200
commit8a031dc29abf1e16b2ee78322a7221b8b5c19a33 (patch)
tree8095b021d3ed73ee9162529a6a3ff4fcbd209a9e /lib/envars.ml
parentf2f146a997e92f3380d9cd9aa0f7aef80f50dba8 (diff)
Fixing unsetting of CoqIDE tags.
Diffstat (limited to 'lib/envars.ml')
0 files changed, 0 insertions, 0 deletions