aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-01-22 20:24:20 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-01-22 20:24:20 -0500
commitfdfeacfad0bba085cb4addd8629ac66a59f123ad (patch)
tree3cb42c7f684ca69c6766fc543409bb14680a26ba /src
parent151b332687fc09496a026481d8ec4fd764b832f2 (diff)
Don't remake .v.d. files in clean-coqprime
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions