diff options
| author | Clément Pit-Claudel | 2019-03-10 19:00:21 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-03-10 19:00:21 -0400 |
| commit | 660732f055021bb4ed3d0a4613aac719cb8f3556 (patch) | |
| tree | 6e5623b6e80e8a356055ad9ea19d63dac6bb39d8 /dev/include_printers | |
| parent | 200a1712b9948fa7682dc95eeb0a520d6804caaf (diff) | |
| parent | 9c201fe42142de7332149863d6c1343c2dec8391 (diff) | |
Merge PR #9654: [sphinx] Add warn option to coqtop directive.
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: vbgl
Reviewed-by: cpitclaudel
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions