Comment 2 for bug 1895521

More specific details:

The text file I'm copy-pasting to stdin is 75572 bytes long.

The total text being transferred consists of the two characters "ml", the text file, and then the control character "^E", i.e. a total of 75575 characters.

Looking through the log file and adding up all the byte counts of writing to file descriptor 3 gives the total sum: 72537 characters. In other words, more than 3000 characters are missing.

Examining the log file some more shows that most of the 4377 different writes to file descriptor 3 consists of just two characters. However, the last 20 or so writes are much larger:

write(3, "3\r", 2) = 2
write(3, "0x8272 0xFFAA\r0x8273 0x0002\r0x82"..., 149) = 149
write(3, "FFA8\r0x827D 0x0003\r0x827E 0xFFA0"..., 207) = 207
write(3, " 0xCF80\r0x828C 0xAAAA\r0x828D 0xF"..., 372) = 372
write(3, "0x82A6 0x0002\r0x82A7 0xE000\r0x82"..., 790) = 790
write(3, " 0xFFAB\r0x82DF 0x0002\r0x82E0 0xE"..., 2095) = 2095
write(3, "x8374 0x0002\r0x8375 0xE000\r0x837"..., 4745) = 4352
write(3, "\r0x84AB 0xC904\r0x84AC 0xFFAB\r0x8"..., 10438) = 4608
write(3, "x85F4 0xC10C\r0x85F5 0xFFAB\r0x85F"..., 11520) = 4608
write(3, "73D 0xFFF8\r0x873E 0x003F\r0x873F "..., 11520) = 4608
write(3, "6 0x003F\r0x8887 0xFFFF\r0x8888 0x"..., 11520) = 4608
write(3, "0x4321\r0x89D0 0x0001\r0x89D1 0x43"..., 11520) = 4608
write(3, "0027\r0x8B19 0xC23E\r0x8B1A 0x8B48"..., 11520) = 4608
write(3, "11\r0x8C62 0x0F80\r0x8C63 0x8765\r0"..., 11520) = 4608
write(3, "\r0x8DAB 0xFFAB\r0x8DAC 0x0020\r0x8"..., 11520) = 4608
write(3, "x8EF4 0xE000\r0x8EF5 0xE000\r0x8EF"..., 11520) = 4608
write(3, "03D 0x00A0\r0x903E 0xCFA0\r0x903F "..., 11520) = 4608
write(3, "6 0x0F82\r0x9187 0x3210\r0x9188 0x"..., 9725) = 4608
write(3, "0x0F82\r0x92D0 0x4567\r0x92D1 0x0F"..., 5117) = 4608
write(3, "0x9481 0x000E\r0x9482 0x00A0\r0x94"..., 509) = 509
write(3, "\5", 1) = 1