diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-12 16:28:10 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-12 16:28:10 +0200 |
commit | 72d9bf028d0cf40cb6c727c69bfbcc15aafc4944 (patch) | |
tree | 4f06742ac395a8021f1a371798f8a6a2330a6384 /.gitignore | |
parent | 3a3f11fe1b6c0f059cf2bd0d71aa4deb4a876b26 (diff) |
Makefile: no more .ml4.d hence no more rule to clean them
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions