<html><head><meta http-equiv="content-type" content="text/html; charset=us-ascii"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><br>
<div><br><blockquote type="cite"><div>On 24. Jul 2024, at 16:15, Norbert Schirmer <nschirmer@apple.com> wrote:</div><br class="Apple-interchange-newline"><div><div style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;">There is at least one commit in the development version that could have changed the behaviour:</div><div style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><a href="https://isabelle-dev.sketis.net/rAFPb626e627c3cb280b4fb609d9ebebe1e905930f83">https://isabelle-dev.sketis.net/rAFPb626e627c3cb280b4fb609d9ebebe1e905930f83</a></div></div></blockquote></div><br><div>I have meanwhile confirmed on my machine that this is actually the changeset that introduces the problem.</div><div><br></div><div> Regards,</div><div><br></div><div> Norbert</div><div><br></div></body></html>