aboutsummaryrefslogtreecommitdiff
path: root/reproduce/software/patches/valgrind-3.15.0-mpi-fix1.patch
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2020-06-03 19:37:48 +0100
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2020-06-03 20:00:28 +0100
commita69f2ce5624b0b683b793a2f4cb68c7023458f15 (patch)
treebf103ae11ba66ba658813d954d92b987d2097eb8 /reproduce/software/patches/valgrind-3.15.0-mpi-fix1.patch
parent3d8aa5953c4e0b79278ab2e27ec4e1051310d04f (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