gen_docs

#!/usr/bin/env bash
link=0
site_root='/'
while [ "$1" != "" ]; do
    case $1 in
        -t | --target )           shift
                                target=$1
                                ;;
        -r | --source )           shift
                                source=$1
                                ;;
        -w | --web )            shift
                                site_root=$1
                                ;;
        -l | --link )    link=1
                                ;;
        * )
                                exit 1
    esac
    shift
done
if [ -z "$source" ]; then
  source=_target/deps/mathlib/
fi

args=()
if [ -n "$target" ]; then
  args+=( '-t' )
  args+=( "$target" )
fi
if [ "$link" -eq "1" ]; then
  args+=('-l')
fi

bash "$source"scripts/mk_all.sh
lean src/entrypoint.lean >export.json
bash "$source"scripts/rm_all.sh

python3 print_docs.py -r "$source" -w "$site_root" "${args[@]}"