diff options
| author | Pierre Courtieu | 2019-05-22 11:04:56 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2019-05-22 11:04:56 +0200 |
| commit | bb2e058a83a4e49e27f5eabe5946926f90fb61b2 (patch) | |
| tree | a5eace0ecedb13f0691a35077ee421d819caa26d /generic | |
| parent | 946be87a944c9d8b850fdddb83d36e2ef9dad5c9 (diff) | |
FIX #422.
the output of coqtop-help is now stored in a variable like coq's version.
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions