#!/bin/bash set -e function redir { mkdir -p "$(dirname "$1")" cat < "$1"

Redirecting to $2...

EOF } if [ -e public ]; then rm -r public fi redir public/index.html "https://docs.rs/rug/" redir public/rugint/index.html "https://docs.rs/rug/*/rug/integer/index.html" redir public/rugint/struct.Integer.html "https://docs.rs/rug*/rug/struct.Integer.html" redir public/rugrat/index.html "https://docs.rs/rug/*/rug/rational/index.html" redir public/rugrat/struct.Rational.html "https://docs.rs/rug/*/rug/struct.Rational.html" redir public/rugflo/index.html "https://docs.rs/rug/*/rug/float/index.html" redir public/rugflo/struct.Float.html "https://docs.rs/rug/*/rug/struct.Float.html" redir public/rugcom/index.html "https://docs.rs/rug/*rug/complex/index.html" redir public/rugcom/struct.Complex.html "https://docs.rs/rug/*/rug/struct.Complex.html" find ../gmp-mpfr-sys/target/doc/gmp_mpfr_sys -name \*.html | while read f; do file="${f#../gmp-mpfr-sys/target/doc/}" redir "public/$file" "https://docs.rs/gmp-mpfr-sys/*/$file" done # rewrite top index to point to root redir public/gmp_mpfr_sys/index.html "https://docs.rs/gmp-mpfr-sys/" find ../gmp-mpfr-sys/public/ -name \*.html | while read f; do file="${f#../gmp-mpfr-sys/public/}" redir "public/$file" "https://tspiteri.gitlab.io/gmp-mpfr-sys/$file" done