diff options
| author | Maxime Dénès | 2018-03-16 00:53:57 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-16 15:13:39 +0100 |
| commit | efcff2e4ae6cabaf90fec1d5bd0cec0f5d4a3a4a (patch) | |
| tree | 445e4579c0d2916400088181f392b93185a35f85 /dev | |
| parent | 1b462cfd2b03fa90e30b6d53de3adb33bc756eaf (diff) | |
[Sphinx] Better error message for coqtop errors
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions