diff options
| author | Jason Gross | 2020-04-19 14:17:58 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-04-19 14:43:55 -0400 |
| commit | ff293b3564efec8c911c3df9cd3a71863161d8b3 (patch) | |
| tree | b4d3c9825176246197140239d211de9b8e6b9907 /kernel/nativelambda.ml | |
| parent | 8d3f4fcd162c7dd23619f605d55e9a773c131e0e (diff) | |
Fix Makefile warning: undefined variable '*'
We fix
```
Makefile.build:222: warning: undefined variable '*'
```
by not passing a time format including a Makefile variable when not
inside a target (and whether or not the command succeeds should not
depend on the particular format in any case, and all we are testing for
is whether or not the command exists and supports `-f`).
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions