Skip to content

Add colour to defunct-readme.sh and ignore .git#3086

Open
silas-hw wants to merge 1 commit into
agda:masterfrom
silas-hw:colour-readme-ci
Open

Add colour to defunct-readme.sh and ignore .git#3086
silas-hw wants to merge 1 commit into
agda:masterfrom
silas-hw:colour-readme-ci

Conversation

@silas-hw

@silas-hw silas-hw commented Jul 23, 2026

Copy link
Copy Markdown
Contributor

Adds some beautiful colourings to the output of defunct-readme.sh, which is purely cosmetic (namely file names are made bold and errors are made red).

In the process of testing these changes, I found that grep was checking through the .git folder for references to deleted READMEs, which I'm pretty sure is unwanted, thus .git has been set as an exclude-dir when calling grep.

@jamesmckinna

Copy link
Copy Markdown
Collaborator

Should this be rolled into #3080 ? or is it really 'separate'.

As for:

... some beautiful colourings

that's usually a matter for others to decide! ;-)

@silas-hw

Copy link
Copy Markdown
Contributor Author

To me it seemed separate enough, at least the colour part is. I can roll it into the other PR tomorrow if it's easier to manage though!

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.

2 participants