
<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">

><br>

<div style="color: rgb(0, 0, 0);">

<div>

<div dir="ltr">

<div>Could you point me to your test and instructions on how to reproduce this problem?  We might get lucky and I'll be able to fix.</div>

<</div>

<div dir="ltr"><br>

</div>

<div dir="ltr">Thanks. It'll take a bit of work because it's a big project, so I'll need to put together instructions, but I'll see if  can create a script that downloads, builds and sets everything up for you so that you can do the minimum. I'll let you know

 when I've done it.</div>

<div dir="ltr"><br>

</div>

<div dir="ltr">(If there is a cray machine anywhere that both of us have access to ... please let me know).</div>

<div dir="ltr"><br>

</div>

<div dir="ltr">JB</div>

<div dir="ltr"><br>

</div>

</div>

</div>

</div>

</body>

</html>