Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

Deal with changing filenames #30

Open
chris321 opened this issue May 24, 2011 · 1 comment
Open

Deal with changing filenames #30

chris321 opened this issue May 24, 2011 · 1 comment
Labels
enhancement important

Comments

@chris321
Copy link
Collaborator

Changes to the code/original judgments could result in some judgments being moved to different locations. We should add links or redirects in this case since someone may have linked to the old location.

This is probably unlikely to occur in practice, but it should be easy to take care of.
@chris321
Copy link
Collaborator Author

Actually it's slightly more problematic - simply rebuilding without changing anything could cause some files to move.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement important
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@chris321