diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-06 14:37:32 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-08 14:37:36 +0200 |
| commit | 0c112c91d6a4756bacc19b12a8c2351053093fb4 (patch) | |
| tree | d35fb4240976f1970874edd9f6bd538fa00bae3d /Makefile.ide | |
| parent | 1d6d0060330197896748739a625d0b1c7f083da2 (diff) | |
Makefile: make clean now removes the .coq-native subdirs
More precisely, we first remove *.native, *.cm*, *.o, which should
normally consistute the only content of these .coq-native directories,
and then remove these directories if they're indeed empty
Diffstat (limited to 'Makefile.ide')
0 files changed, 0 insertions, 0 deletions