diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-08-21 15:30:48 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-08-21 15:30:48 +0200 |
commit | 7db02b704b9b99e364d23f5ac4ed24594a31f88e (patch) | |
tree | 20c11e6d69a6a588956b528546f08988c640bb97 /.gitignore | |
parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) |
Fix coqdoc test-suite target on Windows.
Commit 8f12597 introduced new output tests but these were broken on Windows.
We fix them by using --strip-trailing-cr option of diff, like in other
output tests in the test-suite.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions