aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-31 15:15:32 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-31 15:15:32 +0200
commit88a632b508977966b1e8d4f4449824a55ffc65d1 (patch)
tree793d2274b8a9bf72be57dd3296b69f0c9eaba21c /tools/coq_makefile.ml
parentac8a84e3b4dc530b000e17b72c7e26f7a957420f (diff)
parent3ce7ae5c2de955d5d79fc23a02ee06fa9071f24a (diff)
Merge PR #7401: Automatically run alienclean before compiling.
Diffstat (limited to 'tools/coq_makefile.ml')
0 files changed, 0 insertions, 0 deletions