diff options
author | 2017-06-29 14:56:36 -0400 | |
---|---|---|
committer | 2017-06-30 13:16:54 -0400 | |
commit | d83bd63441d313b6dabe71cae647b1950c621cf6 (patch) | |
tree | 2651efaba54a87d1e1fb38cf28d94eae64722500 /configure.ml | |
parent | 35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff) |
Better support for make TIMED=1 on Windows
This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions