document .gitignore. Add .DS_Store to it while at it.

plfa / plfa.github.io

An introduction to programming language theory in Agda

https://plfa.github.io

Creative Commons Attribution 4.0 International

1.36k stars 307 forks source link

document .gitignore. Add .DS_Store to it while at it. #1025

Open JacquesCarette opened 1 month ago

JacquesCarette commented 1 month ago

As per title.

JacquesCarette commented 1 month ago

So it seems to pre-commit hook didn't like my changes to .gitignore. Are the rules to obey written down somewhere?

wenkokke commented 1 month ago

The pre-commit setup sorts it alphabetically, which is incorrect given that .gitignore exclusions and inclusions are order-dependent, so that should probably be taken out.

(The details are in the pre-commit config file. Follow the links to the various repositories to find out what code each action runs.)