diff options
| author | Enrico Tassi | 2019-02-21 15:07:45 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-27 13:06:59 +0100 |
| commit | 262fae6050ec892bb71936978c84178a12cddc36 (patch) | |
| tree | 9e8c0029075d54b2260c59bcb3d99b0b6ee8f1a7 /dev | |
| parent | 9d6f268723b6352a97bcc3baf0df57f1c1b251fa (diff) | |
[ide] only use Coq_config for the URL of the manual
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions