Skip to content

Add tool to scan for references of deleted or renamed READMEs#3041

Open
silas-hw wants to merge 10 commits into
agda:masterfrom
silas-hw:defunct-readme
Open

Add tool to scan for references of deleted or renamed READMEs#3041
silas-hw wants to merge 10 commits into
agda:masterfrom
silas-hw:defunct-readme

Conversation

@silas-hw

Copy link
Copy Markdown
Contributor
  • Added .github/tooling/defunct-readme.sh, which compares the current branch against master to see if any READMEs have been deleted, and if so scans for references to that README in other files. If any are found, the script exits with an error
  • CI hasn't been modified to use it yet
  • Currently the script exits on the first error, but it shouldn't be hard to update it to list all errors before exiting
  • Partially addresses Add checks for defunct and orphaned READMEs to CI #3037

@silas-hw silas-hw changed the title Add tool to scan for references to deleted or renamed READMEs Add tool to scan for references of deleted or renamed READMEs Jun 30, 2026

@JacquesCarette JacquesCarette left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have not done shell scripting in far, far too long, so my 'approve' should be considered fairly weak. I see no immediate problem here, BUT... (Of course, I do think that the idea is good and helpful.)

@gallais gallais left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not a huge fan of the fact that master is hard coded in the script.
E.g. when we (rarely) are merging into experimental, master's status is irrelevant.

Comment thread .github/tooling/defunct-readme.sh Outdated
Comment thread .github/tooling/defunct-readme.sh Outdated
@silas-hw silas-hw requested a review from gallais July 2, 2026 14:48
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.

3 participants