Skip to content

Comments

Rename files with & in their name#20

Open
masinter wants to merge 1 commit intomainfrom
rename-ampersands
Open

Rename files with & in their name#20
masinter wants to merge 1 commit intomainfrom
rename-ampersands

Conversation

@masinter
Copy link
Member

@masinter masinter commented Feb 5, 2026

normally files that are "latest" and corresponding to the source code also go in the repo, while older versions belong in some other storage, not to be edited and findable through thte bibliography.

So maybe the files should have been deleted? or make taht a separate issue?

This PR just fixes the probem that HCFILES doesn't deal well with file names containing &. (ampersand)

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.

1 participant