Issue: & replaced by <body> in inserted navbar #111
Description
When inserting our navigation bar HTML via insert_navbar.sh on GitHub Actions, entities like ☰ get mangled into <body>#9776;. This doesn’t happen locally in my WSL Ubuntu. It seems that the GitHub Actions shell is interpreting the HTML differently and replacing & with . This is happening in repos that have built docs in the last 24 hours (or maybe more), I guess GitHub is changing its environments and new one escaped special characters in another way. This issue is causing issue like Libraries nav item is not clickable in DynamicPPL and JuliaBUGS!
Solution is to switch from naive string replacement to an awk-based insertion. This should prevent the shell from altering special characters.
And, why are we not using TuringLang/actions
I am opening PRs for both repos, this one and actions.