diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-07-19 14:28:45 -0700 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-07-19 14:28:45 -0700 |
| commit | d47273cea29099c296e1b702ab25aa8272ab6831 (patch) | |
| tree | 940f9f34a116aeda7b93bc4e75470bf8292d19f3 /engine | |
| 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 'engine')
0 files changed, 0 insertions, 0 deletions