You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
loads packages before plugins to prevent failures in dune loader (#1573)
If bundled plugins are loaded before dune packaged plugins, the latter
will fail on modules that were linked by the former. The old bap plugin
system has now way to notify the dune plugin system on what units are
loaded (no worries the dynlink system used by both will prevent
double-loading). Instead of catching the Unit_already_loaded exception
from dune, we better first load all dune packages and only after that
handle the old bundled plugins with our old loader, which is capabled
of handling correctly this exception.
0 commit comments