diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-07-05 09:36:15 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-05 09:36:15 +0200 |
commit | 2afc76653cbe6b8775e82cdc1a6d6985b33643b4 (patch) | |
tree | 5394dda254053e2ac2ac0d77c5ec4a29f366fbc9 /plugins | |
parent | 8155ba54ae39dd71c6b8ddff2b2b7353dde9aff8 (diff) | |
parent | 2af4433ad83a51e31cd845784afb12032767441f (diff) |
Merge PR #832: Document an example `Makefile` for `coq_makefile`
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions