aboutsummaryrefslogtreecommitdiffhomepage
path: root/man
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-01 13:48:47 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-06 22:31:20 +0100
commited98716036e9d47efb2ba66cf0336fc45e03f793 (patch)
tree10866ccd6be614ad70b92d4609139db534af8bf7 /man
parent7e0eeba3e91cd5da029aaa6b9c86f7a13f505b88 (diff)
Closes #6830: coqdep reads options and files from _CoqProject.
Note that we don't look inside -arg for eg -coqlib.
Diffstat (limited to 'man')
0 files changed, 0 insertions, 0 deletions