Today I checked with a DSO: ISR duration is almost exactly 123 microseconds for each and every period the DSO captured. I tried to trigger on >130 microsecond hi pulses but got not trigger condition. --> no pulse exceeds 130 microseconds
Then I triggered on >950 microseconds low pulses --> it does not trigger --> seems it does not drop any interrupt.
I conclude that this looks like a bug in my code and the ISR seems to work fine. However this would imply that adding the prints somehow makes my code glitch. Very strange.