diff options
| author | Hugo Herbelin | 2020-04-22 21:33:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-22 21:33:08 +0200 |
| commit | 7e2167f5bfd7d70847d1b1ece34c1f0303f46fc8 (patch) | |
| tree | 14cdfee31f459cc7b4b195c4c14ca241db21ccbb /dev/include | |
| parent | 036051077d638317f27f727b7c551a9a1b7886b7 (diff) | |
| parent | f952c8c45a51acf9155b81839db4f3d0ab6e7aa1 (diff) | |
Merge PR #11928: Remove probably useless doc/sphinx/coqdoc.css.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions