On 03/10/2024 08:47, Eli Zaretskii wrote: >>> If Hg doesn't prepend fake leading directories, we don't need to be >>> bothered by Hg. >> >> It does. A fuller example, with deletion: This was file creation, btw. Just to keep the things clear. >> diff -r d045d1125783 -r 9396bae6ff0d CLOBBER.new >> --- /dev/null Thu Jan 01 00:00:00 1970 +0000 >> +++ b/CLOBBER.new Fri Dec 15 20:37:14 2023 +0200 >> @@ -0,0 +1,56 @@ > > OK, then does the presence of two -r options indicate Hg? Or is that > not guaranteed, either? No guarantee I suppose, but I'm not aware of any others, yet. And apparently 'hg diff --git' can also output diff --git a/a b/b But that seems fine for our check. >> I'm concerned the user is going to wonder whether anything happened at >> all, and checking is a non-trivial action. But if you think this is >> fine, I guess it's something to try. > > Not sure I understand the problem. The user instructed us to apply > diffs, one of which deletes a file. Why should we hesitate about > deleting that file? It's a destructive operation, not always easy to undo. The current edits might be saved to disk but not checked in, for example. I suppose using a prompt could be enough, though. >>>> Deleting files is something that one can do manually, though, so solving >>>> this seems lower priority. >>> >>> When you apply a large set of diffs in which one file is deleted, >>> there's no easy way of knowing you should deleted that file. >> >> In the current version of code you will be asked midway through a file >> (or right away, when using diff-apply-hunk) to specify a file name, >> defaulting to /dev/null, and after you press C-g after seeing the odd >> prompt the hunk won't be applied. So it's hard to miss, at least. > > Yes, but this is buggy behavior: there's no need to ask for a file > name in this case. Emacs is just confused by the part of the diffs > which delete a file because the code doesn't take that into account. All right, the attached seems to support both creation and deletion, including applying hunks in reverse direction. Things got trickier but not by a lot.