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