Skip to content

Improve handling of subdirs for git extra-deps#56

Merged
cdepillabout merged 1 commit into
mainfrom
fix-git-extra-deps-subdirs
Nov 11, 2024
Merged

Improve handling of subdirs for git extra-deps#56
cdepillabout merged 1 commit into
mainfrom
fix-git-extra-deps-subdirs

Conversation

@cdepillabout
Copy link
Copy Markdown
Owner

@cdepillabout cdepillabout commented Nov 11, 2024

This is just a rebase of #46 into main.

Closes #45.

@cdepillabout
Copy link
Copy Markdown
Owner Author

Thanks @isomorpheme!

@cdepillabout cdepillabout merged commit 72742cc into main Nov 11, 2024
@cdepillabout cdepillabout deleted the fix-git-extra-deps-subdirs branch November 11, 2024 06:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Approach of copying subdirs for git extra-deps breaks in the presence of relative symlinks

2 participants