diff options
| author | Gaëtan Gilbert | 2019-02-14 14:57:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 21:24:11 +0100 |
| commit | 2e4e082637771bc047fbd977aaa5de26956c4618 (patch) | |
| tree | 10c4dcfda4047eeff0d9859c32df9c51142b8eb4 /doc/sphinx | |
| parent | 7c4d6b904adb4a5d025ebcb804613f558e5b8be9 (diff) | |
coqdomain.py fix typo in comment
Diffstat (limited to 'doc/sphinx')
0 files changed, 0 insertions, 0 deletions