aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/kernel.mllib
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-23 18:06:26 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-23 18:06:26 +0000
commitbdc7217d03a109a9149d7c93bbe2f95b1df480f5 (patch)
treee5629f161ca05baa15552fc7cc06539777d9219b /kernel/kernel.mllib
parent40b00efff7e47b22c80c677514f9d689c918383c (diff)
Coqmktop: missing -I (fix #2851)
The modules used in coqmktop's temporary main file should have their .cmi in the search path, hence a small set of -I is required: lib, toplevel. We do not place their the full list to avoid issues with the win32 command-line length Btw, coqmktop -boot now also builds its list of -I instead of receiving them via its command-line, it's simpler this way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/kernel.mllib')
0 files changed, 0 insertions, 0 deletions