Closed christian-krieg closed 2 years ago
friendly ping :)
Thanks Christian, merged. I wish we could handle the vector changes too, but lazy to do it :-) If only there was a convenient builtin way to make readline read until any whitespace instead: https://stackoverflow.com/questions/47927039/reading-a-file-until-a-specific-character-in-python
Thank you so much, Ciro! Probably we'll add support for the vector changes once we desperately need it :D
Cheers, Christian