diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2014-12-23 02:00:07 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2014-12-23 02:00:07 +0000 |
commit | 424ce5f435a14cbcfc85d333d365d0066106e55b (patch) | |
tree | 7ba1df349c1e08d19d1e7deaccbdc524f4e9f1d4 /CHANGES | |
parent | 13d8ad97def828eb7ee441eec21d1cbd96e5f5b2 (diff) |
Fix a special case in _CoqProject syntax (empty string).
Diffstat (limited to 'CHANGES')
0 files changed, 0 insertions, 0 deletions