aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-10-10 17:05:50 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-10-13 17:48:42 +0200
commite62984e17cad223448feddeccac0d40e1f604c31 (patch)
tree9381260fc64dd7b53cf976ef55c70f2c2a291f88 /library/global.ml
parentc8ca44cf328746636865834843744fea6f73d0d2 (diff)
Coqinit: look in toploop/ even if configured with -local
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions