desktop.ini in gitignore

Stream: general

[Filippo A. E. Nuccio]

I see that @Scott Morrison added a bunch of OS-related files to gitignore in mathlib and I wonder if it would be possible to add desktop.ini. These is a Win config file that customises the Desktop behaviour of the folder (typically, its icon).

[Julian Berman]

People generally don't agree with me (and will do what you're asking for), but just in case you're not aware at least as an interim solution, there is a global git ignore file where you can put all the files you yourself never care about in any repository which you can of course add that to immediately. (E.g. mine is here: https://github.com/Julian/dotfiles/blob/main/.config/git/ignore )

[Filippo A. E. Nuccio]

I certainly was not aware, so thank you!

[Filippo A. E. Nuccio]

But just to understand: where is it exactly? Is it somewhere in your computer and you set up some global git config file informing git to have a look there?

[Julian Berman]

It depends on your OS -- man 5 gitignore will tell you the possibilities

[Julian Berman]

It's ~/.config/git/ignore generally, if you don't set XDG_CONFIG_HOME or know what that is.

[Filippo A. E. Nuccio]

Let me have a look

[Filippo A. E. Nuccio]

Yep! Thanks.

[Filippo A. E. Nuccio]

Actually what I did (on Win 11) was to

1. Create a .gitignore file in my usr folder
2. run (in the git bash) git config — global core.excludesfile ~/.gitignore that added the above file to the gitexclude field of my global gitconfig
3. Inside this gitignore file, add desktop.ini.

Now I can change icons to tracked repository without hurdles.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as resolved.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.

[Filippo A. E. Nuccio]

(marked unresolved just in case someone still wants to add the desktop.ini to the global mathlib gitignore file)