Skip to content
This repository has been archived by the owner on Jun 26, 2024. It is now read-only.

use URI file instead of path so that the scheme gets set properly on windows #258

Merged
merged 1 commit into from
Feb 11, 2021

Conversation

alexjbest
Copy link
Contributor

Go to defintion via widgets was broken for me before this change

The doc at
https://github.com/microsoft/vscode-uri
implies that we should not make this change if we make use of query fragments (i.e. "https://code.visualstudio.com/docs/extensions/overview#fragment") but I don't believe that we do.
Testing on linux/mac would be great, and if anyone who uses some remote development set-up can test that would also be cool!

@gebner gebner merged commit ea0206b into leanprover:master Feb 11, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants