- 
                Notifications
    You must be signed in to change notification settings 
- Fork 5
Description
Currently there are cases where the libs entry of the plugin config points to folders outside of the current workspace. This is a common use case that's valid, and including those files works as expected. However subsequent includes that are contained in those files do not appear to resolve correctly.
For example, if we have a lib file /a/b/c/lib.pli that lives outside of the workspace (let's say our workspace is in /workspace), but we have /a/b/c in our libs entry. Then the following include will resolve from within our workspace:
%include lib
However the following include contained in /a/b/c/lib.pli will not resolve from outside the workspace.
 // inside lib.pli
 %include "some-file-in-my-workspace.pli";
These includes should resolve using the same config in our workspace, regardless of whether the included file is located in that workspace or not.