aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-06 14:57:40 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:28 +0200
commit046657081fb769fcf033c7d7c6b3fb6e861a0996 (patch)
tree4a3287cce1f3fa35f1139e48893f7a5d2a63eb70 /.gitignore
parente94334670c7aa9c96e40d678fcc7a7a70cfd0099 (diff)
ocamlfind: coqtop -config prints ocamlfind as found by ./configure
Used to guess again the ocamlfind location at Coq's execution time. An option to override the value (inferred at ./configure time) is available. So, what is the point of guessing it? Either it stays there, or the user is doing a hack, and has a flag to do it.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions