aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2014-12-23 02:00:07 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2014-12-23 02:00:07 +0000
commit424ce5f435a14cbcfc85d333d365d0066106e55b (patch)
tree7ba1df349c1e08d19d1e7deaccbdc524f4e9f1d4 /CHANGES
parent13d8ad97def828eb7ee441eec21d1cbd96e5f5b2 (diff)
Fix a special case in _CoqProject syntax (empty string).
Diffstat (limited to 'CHANGES')
0 files changed, 0 insertions, 0 deletions