[10:38:01] <FONT COLOR="#008080">---</FONT> <font color="#616161">DominusExult is now known as Dominus</font><BR>
[17:41:16] &lt;<font color="#600060">Dominus</font>&gt; Marzo: I've written you yesterday about it but that was right before you timed out, so you probably didn't see it. Do you have any idea on this? https://github.com/exult/exult/issues/45<BR>
[18:01:00] &lt;<font color="#005000">Marzo</font>&gt; I will have to look<BR>