<html>
<head>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">Before I forget: I did that and it is as
expected; everything still works.</font></p>
<p><font size="+1">Manuel</font><br>
</p>
<br>
<div class="moz-cite-prefix">On 2017-04-25 11:12, Florian Haftmann
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:732e8187-80ea-5ab7-afb7-b7cc030b4e7e@informatik.tu-muenchen.de">
<pre wrap="">Am 25.04.2017 um 11:06 schrieb Manuel Eberl:
</pre>
<blockquote type="cite">
<pre wrap="">I think you actually solved that problem by now. If I recall correctly,
it was one of the two dictionary-related problems I told you about a
year ago or so, and then Lars and you solved that problem somehow.
I can try putting in that code equation again and seeing what happens.
</pre>
</blockquote>
<pre wrap="">
Excellent, thanks.
Florian
</pre>
</blockquote>
</body>
</html>