aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-12 16:28:10 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-12 16:28:10 +0200
commit72d9bf028d0cf40cb6c727c69bfbcc15aafc4944 (patch)
tree4f06742ac395a8021f1a371798f8a6a2330a6384 /.gitignore
parent3a3f11fe1b6c0f059cf2bd0d71aa4deb4a876b26 (diff)
Makefile: no more .ml4.d hence no more rule to clean them
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions