aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre Boutillier2014-09-18 10:57:02 +0200
committerPierre Boutillier2014-09-18 11:00:15 +0200
commit82229da083c2cfecca63f4ff5ca7da41bda059f6 (patch)
tree766c0cef82217907f949e8cdc6ae76515486a768 /dev
parent21335959eac94b9c35424516ef78fd45b6acf551 (diff)
fix coq_makefile
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions