You are viewing a single comment's thread. Return to all comments →
I opened a ticket, but never obtained a satisfactory answer/solution. I worked around the problem by using Scanf, which is anyway more flexible.
read_line works as well, but of course you have to manually call int_of_string on the inputs