To run on Ubuntu 20.04, I had to change the last line of "mario.sh" to:

done) | sed -Enf ./mario.sed