diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-06-03 19:37:48 +0100 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-06-03 20:00:28 +0100 |
commit | a69f2ce5624b0b683b793a2f4cb68c7023458f15 (patch) | |
tree | bf103ae11ba66ba658813d954d92b987d2097eb8 /reproduce/software/patches/valgrind-3.15.0-mpi-fix1.patch | |
parent | 3d8aa5953c4e0b79278ab2e27ec4e1051310d04f (diff) |
README-hacking.md: Improved section on ignoring some files in Maneage
When some files should not be merged, until now we were suggesting to also
add deleted files to the '.gitattributes' file. However, this feature of
Git doesn't work for deleted files and they would still show up in the
'master' branch after a merge.
So with this commit, we have added a simple AWK command to run after a
merge that will automatically detect and delete such files (using the
output of 'git status --porcelain').
Also, two minor typos were corrected in the newly added
'servers-backup.conf' file: the copyright year was wrong and there was no
new-line at the end of the file (a good convention!).
Diffstat (limited to 'reproduce/software/patches/valgrind-3.15.0-mpi-fix1.patch')
0 files changed, 0 insertions, 0 deletions