diff options
| author | Clément Pit-Claudel | 2018-05-04 19:03:25 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-05-15 12:05:44 -0400 |
| commit | b053c575e48c25631cfa6a6a8ed33b6b93c95ea7 (patch) | |
| tree | 351944345410cd3d0b3da80ba09fc275ce930e0b /dev/base_include | |
| parent | d5bb8a4ae2f509532ecfb4a53bb91c64d992c2e6 (diff) | |
[doc] Search for 'coqtop' in $PATH if COQBIN is unset
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions