diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-08-02 13:47:07 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-08-02 13:52:59 +0200 |
| commit | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (patch) | |
| tree | fac80e4ef28e99b205a1699930997b79c23ca292 /man/coqtop.opt.1 | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
Makefile: 'make clean' now immune to the check for binary files without sources
This is a followup of 7d1fc15. Without this fix, you're warned of leftover files,
but even a 'make clean' is then refused, so you cannot get rid of them easily
(apart via a git clean -xfd).
Diffstat (limited to 'man/coqtop.opt.1')
0 files changed, 0 insertions, 0 deletions