diff options
| author | Jason Gross | 2020-04-26 15:44:55 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 13:03:05 -0400 |
| commit | 452f809a580a29626aa36f5f7061aca12f9f458e (patch) | |
| tree | d74337e2d9bb0f1b6416c654c6702f732ba1cd5b /dev/include_dune | |
| parent | ee3b91fe06c72a8ffe92d31a7e40fe54cd71f746 (diff) | |
Work around a bug in Coq in the doc
This is the bug
https://github.com/coq/coq/pull/12129#issuecomment-619613779
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions