diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/library/lib.ml b/library/lib.ml index e8b56de70..e1dd9ae39 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -513,8 +513,14 @@ let close_section () = type frozen = Names.DirPath.t option * library_segment let freeze ~marshallable = - if marshallable = `Shallow then !comp_name, [] - else !comp_name, !lib_stk + if marshallable = `Shallow then + (* TASSI: we should do something more sensible here *) + let _, initial_prefix = + CList.split_when (function _, CompilingLibrary _ -> true | _ -> false) + !lib_stk in + !comp_name, initial_prefix + else + !comp_name, !lib_stk let unfreeze (mn,stk) = comp_name := mn; |