diff options
| author | Maxime Dénès | 2017-11-17 13:57:31 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-11 13:54:35 +0100 |
| commit | e098767a05372bf766b7d8e67e4acb623d5b2abf (patch) | |
| tree | 873d9fea655409c45ce3db4043b0c88935ca5e08 /kernel | |
| parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) | |
Restoring filtering of native files passed to `rm` during `make clean`.
Was lost during the coq_makefile 1 -> 2 translation.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions