diff options
| author | Maxime Dénès | 2015-09-13 11:18:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-09-13 11:23:46 +0200 |
| commit | 0528c147a9eee25668252537905d0c09ec20e3cd (patch) | |
| tree | db289c8a5eb1183204a12e730c1bd34a64858908 /kernel | |
| parent | 7df0761305778270fe569c0942e7079a803d57e9 (diff) | |
Coq_makefile: read TIMED and TIMECMD from environment.
Useful e.g. with submakefiles.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions