aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorppedrot2013-09-19 14:47:23 +0000
committerppedrot2013-09-19 14:47:23 +0000
commit736ffcea3a04da40ea3047216864ca420f220fe5 (patch)
tree84f14a48b0071aaae5616e8b8f1efc382e294f91 /kernel/type_errors.ml
parent826eb7c6d11007dfd747d49852e71a22e0a3850a (diff)
Made the filename of compiled files explicit, i.e. add a ./ prefix
whenever the filename was given alone. This caused strange behaviour of coqtop that was compiling stuff we didn't want to just because it was somewhere in its loadpath. This is why FingerTree was not compiling, btw, as it had two files equally named in two different paths. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16788 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions