FYI, `sudo apt install gawk` can avoid this problem. Debian Bug: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=933934
FYI, `sudo apt install gawk` can avoid this problem. /bugs.debian. org/cgi- bin/bugreport. cgi?bug= 933934
Debian Bug: https:/