Am 17.12.2012 um 16:19 schrieb Makarius: > "If the revision being repaired was part of an applied patch queue" could > also mean the row of changes by Jasmin that were already pushed and in their > proper place. Jasmin, do you remember if these where plain first-order > commits on your side, or the result of applying a patch queue?
Almost certainly queues, with the usual "qfinish -a", "push" sequence. Jasmin _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
