Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Extract project files tracking into function #1319

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

jwortmann
Copy link
Contributor

I noticed that the drive letter normalization from my PR #1313 was incomplete and also needs to be added for the environment changing via julia/activateenvironment here:

# Add project files separately in case they are not in a workspace folder
if server.env_path != ""
for file in ["Project.toml", "JuliaProject.toml", "Manifest.toml", "JuliaManifest.toml"]
file_full_path = joinpath(server.env_path, file)
uri = filepath2uri(file_full_path)
if isfile(file_full_path)
# Only add again if outside of the workspace folders
if all(i->!startswith(file_full_path, i), server.workspaceFolders)
if haskey(server._files_from_disc, uri)
error("This should not happen")
end
text_file = JuliaWorkspaces.read_text_file_from_uri(uri, return_nothing_on_io_error=true)
text_file===nothing || continue
server._files_from_disc[uri] = text_file
if !haskey(server._open_file_versions, uri)
JuliaWorkspaces.add_file!(server.workspace, text_file)
end
end
push!(server._extra_tracked_files, filepath2uri(file_full_path))
end
end
end

This exact same code is used in two places, so I extracted it into a new function track_project_files! (the diff for misc.jl on GitHub is unfortunately a bit misleading).

@jwortmann
Copy link
Contributor Author

I split the PR up into 2 commits, to make it easier to review. I'd recommend to squash the commits when merging.

@jwortmann
Copy link
Contributor Author

It would be great if this PR could be merged, because this bug is currently blocking the update of the server for clients that use uppercase drive letters.

@jwortmann
Copy link
Contributor Author

Bump 🤷

Does anybody read issues and pull requests in this repository and is able to merge this?
The changes are really simple and it shouldn't take more than two minutes or so to review.

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant