Hi, usually you would apply this commit first before reverting the
change. Otherwise you have commits in the middle that don't pass CI.
But that's a nitpick. Thanks for cleaning this up.
Felix
> --
> You received this message because you are subscribed to the Google Groups "isar-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to isar-users+...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/isar-users/20260423121941.1704827-3-wzh%40ilbers.de.