diff options
author | 2016-07-19 14:28:45 -0700 | |
---|---|---|
committer | 2016-07-19 14:28:45 -0700 | |
commit | d47273cea29099c296e1b702ab25aa8272ab6831 (patch) | |
tree | 940f9f34a116aeda7b93bc4e75470bf8292d19f3 /dev/printers.mllib | |
parent | 522bcd72a567a3ae29162519a9a9736581367251 (diff) |
Allow `STDTIME=foo make`
This gives better behavior both when including the `coq_makefile` `Makefile` into other `Makefile`s and when setting `STDTIME` through an environment variable.
Diffstat (limited to 'dev/printers.mllib')
0 files changed, 0 insertions, 0 deletions