aboutsummaryrefslogtreecommitdiffhomepage
path: root/man/coq_makefile.1
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-25 12:25:35 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-25 14:00:44 +0200
commit8e25e107a8715728a7227934d7b11035863ee5f0 (patch)
treeee6b252104ffa6bdd8b47ca87c2148fefe08e048 /man/coq_makefile.1
parent3930c586507bfb3b80297d7a2fdbbc6049aa509b (diff)
The -require option now accepts a logical path instead of a physical one.
Diffstat (limited to 'man/coq_makefile.1')
0 files changed, 0 insertions, 0 deletions