diff options
| author | Maxime Dénès | 2018-06-21 17:46:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-21 17:46:00 +0200 |
| commit | 4a3697da7be172c1559588d326a2f02c80bb98e9 (patch) | |
| tree | e19052e708a1950431f30d80e0f2716b89a0a1e2 /dev | |
| parent | 41cf6afdb70b073838bd2a1e71f76c600e03c006 (diff) | |
| parent | 5808915bcb5f9800727cc10e5232c8983e1842bd (diff) | |
Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understands.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions