Richard Kreiss propounded (on Mon, May 11, 2015 at 03:48:59PM +0000): | Mark's suggestion about copying a file to a new location when unsure | if it is necessary is a good one. You could also just leave it where it is, but rename it. -- JP