diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-17 16:34:59 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-17 16:34:59 +0200 |
| commit | 7451651a70be86ef8f510faabcba445766595187 (patch) | |
| tree | e0511a0bb498049266faf5098dd1780992e96f5a /vernac/vernac.mllib | |
| parent | 88226ad302d4c128173644fc9d992ada67ba6d9c (diff) | |
| parent | 6d5e0dd693e8e7322465323dc8eed4bea1ddce21 (diff) | |
Merge PR #490: A possible fix for #5391 (command line tools do not accept trailing / and \ on windows)
Diffstat (limited to 'vernac/vernac.mllib')
0 files changed, 0 insertions, 0 deletions