diff options
| author | Maxime Dénès | 2017-05-09 09:06:37 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-09 09:06:37 +0200 |
| commit | 98b6ccc4ffa2378e333961f9a59eb7ab0d174ee5 (patch) | |
| tree | e076a7888249368f09a8e7ee77d644c3cf745f4b /dev/include | |
| parent | dc1bae5ff63ca71e80bf0ee19a643b5cb5b284b9 (diff) | |
| parent | cf0e030f3aebecb316852fc4a152fb212f9e7ef5 (diff) | |
Merge PR#615: coqtop -help: don't die if coqlib can't be found
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions