# Skript zum Anpassen von index.html.

cat > mkhtml_index.sed <<EOF
/href=".*\.html"/ {
  s|pcre_||
  /jit_/ {
    s|jit_|jit|
    s|stack_|stk_|
  }
  /context_/ {
    s|context_|ctxt_|
    s|match_|m|
    s|general_|g|
    s|compile_|c|
  }
  /data_/ {
    s|data_|dat_|
    s|match_|m|
    /from_/ s|create_|cr_|
  }
  /get_/ {
    s|ovector_|ov_|
    s|_string|_str|
  }
  /set_/ {
    /compile_/ !s|recursion_|rc_|
  }
  /serialize_/s|serialize_|serial|
  /substring_/ {
    s|substring_|s|
    s|copy_|cpy|
    s|get_|get|
    s|length_|len|
  }
}
EOF

sed -f ./mkhtml_index.sed ../doc/html/index.html > ./index.txt
mv -vf ./index.txt ../doc/html/index.html
rm -vf ./mkhtml_index.sed
