On 09/17/2014 04:48 PM, Pavel Emelyanov wrote: > No problem. Would you send a patch, so I could just apply one? I would if I knew how to do this. You mean sending a diff via mail? Never done anything with github, sorry. Matthias -- Matthias Neuer Universität Ulm kiz / Abteilung Infrastruktur