aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-07-05 15:18:44 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-07-05 15:24:06 +0200
commit618dce7fbf7c5b3ed80dacd16be761c4f7487079 (patch)
treeb14bf1e76fb78a39c6289aed74a542eb78e5e44f /tools/coq_makefile.ml
parenta91bafa58710777506dc30afb1a0e2cc56b941c7 (diff)
Add mailmap entry.
Diffstat (limited to 'tools/coq_makefile.ml')
0 files changed, 0 insertions, 0 deletions