aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/states.ml')
-rw-r--r--library/states.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/states.ml b/library/states.ml
index 906ebdacc..9d15dfc6c 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -28,8 +28,8 @@ let (extern_state,intern_state) =
raw_extern s (freeze())),
(fun s ->
let s = ensure_suffix s in
- unfreeze
- (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
+ let paths = Loadpath.get_paths () in
+ unfreeze (with_magic_number_check (raw_intern paths) s);
Library.overwrite_library_filenames s)
(* Rollback. *)