aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-05-14 16:38:21 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-05-14 16:38:21 +0200
commit3fb81febe8efc34860688cac88a2267cfe298cf7 (patch)
tree1b36449d1bdb7aa29be30cda15d63d36134f2a56 /theories/Lists
parent5f8dc36fb2d65699233b9ac9a3ff9f93701a01cb (diff)
Do not regenerate .d files when cleaning them. (Fix bug #4079)
Diffstat (limited to 'theories/Lists')
0 files changed, 0 insertions, 0 deletions