On 03.11.18 09:40, j...@tcs.ifi.lmu.de wrote:
> @Matthias Urlichs: The file had been comitted to the repository
> initially. It was only added to .gitignore much later on, when other
> users complained.
Ah. Sorry, I missed that.
You're right – this is a bug. My reasoning for that assessment is th
@Matthias Urlichs: The file had been comitted to the repository initially.
It was only added to .gitignore much later on, when other users complained.
@Philip Oakley: The files in question are local configuration files (for my
editor, which contained private ssh settings for testing the code tha
> The file is added to .gitignore
I'm not sure why this step of adding the name of an important file to
the ignore list was added. To me, that sounds a bit backward. Usually,
an important file would not be listed in the ignore file.
Would you be able to expand on the reason for the adding t
On 02.11.18 18:12, j...@tcs.ifi.lmu.de wrote:
> The file is heavily edited, but ignored by commits as expected.
Last time I checked (which was half a minute ago), files in .gitignore
are only ignored for the purpose of not adding them to the archive.
Modifying such a file, editing it, and then "g
