-
Notifications
You must be signed in to change notification settings - Fork 469
Remove cmij cache #6192
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Remove cmij cache #6192
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -27,7 +27,7 @@ let init_path () = | |
let exp_dirs = | ||
List.map (Misc.expand_directory Config.standard_library) dirs | ||
in | ||
Config.load_path := List.rev_append exp_dirs []; | ||
Config.load_path := List.rev_append exp_dirs [Config.standard_library]; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Interesting. Presumably this must have been there a long time ago. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Without this, the CMI files (that were formerly loaded from the cache) are not found. |
||
Env.reset_cache () | ||
|
||
(* Return the initial environment in which compilation proceeds. *) | ||
|
This file was deleted.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!