
<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">

<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>

</head>

<body dir="ltr">

<div id="divtagdefaultwrapper" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Helvetica, sans-serif, EmojiFont, "Apple Color Emoji", "Segoe UI Emoji", NotoColorEmoji, "Segoe UI Symbol", "Android Emoji", EmojiSymbols;" dir="ltr">

<p style="margin-top:0;margin-bottom:0">Hi Christophe,</p>

<p style="margin-top:0;margin-bottom:0"><br>

</p>

<p style="margin-top:0;margin-bottom:0">I tried using the latest git version a couple of days ago. I did not see any changes in this regard. </p>

<p style="margin-top:0;margin-bottom:0"><br>

</p>

<p style="margin-top:0;margin-bottom:0">Anthony</p>

</div>

</body>

</html>