dec56f1548
last version and (2) remove a disabled debugging fprintf() that I accidentally committed here. Noticed by: simon (2)