aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorPierre Boutillier2014-09-01 10:28:38 +0200
committerPierre Boutillier2014-09-03 14:24:05 +0200
commitd34cb7cc523fe7f6e9b371cee17b7f7b7e588ddf (patch)
tree81353fa9c918c588f9eaa297486f4499f4e5607a /plugins
parent81b43a0c8137dc890fe1eb462cf278c39cac3a5f (diff)
Improve RefMan section about Coq_makefile
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions