Am 12.02.2014 um 16:03 schrieb Makarius <makar...@sketis.net>: > I see a lot of incoming changes (and many hg queue accidents) just before > that,
The "accidents" were that I experimented with "qfold" for the first time. The command merges two patches together. The patches themselves were all as I intended them to be, and the extra pass I applied to reorder and merge the patches was well worth it. What I didn't notice until it was too late was that after merging, the messages were merged as well (with " * * * " and in a multiline style). I had expected only the description of the parent patch (the one that's merged into) to appear. The one-line format used for displaying descriptions encouraged my misbelief. To those who use queues and don't know about "hg qpush --move" and "hg qfold" (which didn't exist some years ago): Those are very useful tools, when used correctly. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
