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