fixlinks.sh (2227B)
1 #!/usr/bin/env bash 2 3 set -euET -o pipefail 4 5 # Scribble (in Racket 7.3 at least) incorrectly redirects some local links within the page to a remote server, this restores the links back to local. 6 # Replace "https://docs.racket-lang.org/local-redirect/index.html?doc=phc-thesis&rel=index.html%23…" 7 # with a single # 8 # and translate back the %25 escape sequences in the URL 9 # sed can't do a replacement within the matched pattern & and my perl is rusty… 10 11 set -x 12 sed -i -e 's~X~XA~g' doc/phc-thesis/index.html 13 sed -i -e 's~Y~XB~g' doc/phc-thesis/index.html 14 tr \\n Y < doc/phc-thesis/index.html > doc/phc-thesis/index.html2 15 mv doc/phc-thesis/index.html2 doc/phc-thesis/index.html 16 sed -i -e 's~"https://docs\.racket-lang\.org/local-redirect/index\.html[?]doc=phc-thesis&rel=index\.html%23\([^"]*"\)~"#\nXC\1\n"~g' doc/phc-thesis/index.html 17 sed -i -e '/^XC/s~%25~XD~g' doc/phc-thesis/index.html 18 if grep 'XC.*%' doc/phc-thesis/index.html; then 19 echo "Error: some urlencoded escape code was not properly filtered by fixlinks.sh" 20 exit 1 21 fi 22 tr -d \\n < doc/phc-thesis/index.html > doc/phc-thesis/index.html2 23 mv doc/phc-thesis/index.html2 doc/phc-thesis/index.html 24 sed -i -e 's~Y~\n~g' doc/phc-thesis/index.html 25 sed -i -e 's~XD~%~g' doc/phc-thesis/index.html 26 sed -i -e 's~XC~~g' doc/phc-thesis/index.html 27 sed -i -e 's~XB~Y~g' doc/phc-thesis/index.html 28 sed -i -e 's~XA~X~g' doc/phc-thesis/index.html 29 30 # Transform 'href="index.html#…' to 'href="#…' so that links within the page don't cause a reload if the URL was …/phc-thesis/ vs. …/phc-thesis/index.html 31 sed -i -e 's/href="index.html#/href="#/g' doc/phc-thesis/index.html 32 33 cp doc/phc-thesis/index.html doc/index.html 34 sed -i -e 's~"../pdf/~"pdf/~' doc/index.html 35 sed -i -e 's~"../phc-thesis-/~"phc-thesis-/~' doc/index.html 36 set +x 37 for i in doc/phc-thesis/*; do 38 escaped_name="$(basename "$i" | sed -e 's~[]$.*/[\^]~\\&~g' )" 39 sed -i -e 's/\(href\|src\)="'"\($escaped_name\)"'"/\1="phc-thesis\/\2"/g' doc/index.html 40 done 41 set -x 42 43 sed -i -e '1i<!-- This file is a copy of ../index.html with the relative URLs adjusted, it is kept here so that the old URL …/phc-theis/index.html keeps working but the new URL …/index.html should be used. -->' doc/phc-thesis/index.html