if [[ -x "$(command -v unbuffer)" ]]; then
UNBUF="unbuffer"
UNBUF_P="unbuffer -p" else
UNBUF=
UNBUF_P= fi
cd docs/
mkdir -p source/_static
$UNBUF make html-no-doxy 2>&1 | $UNBUF_P grep -v --color=always "WARNING: Duplicate declaration\|WARNING: Inline emphasis start-string without end-string.\|WARNING: Too many template argument lists compared to parameter lists\|^\s*libsemigroups\|Citation .* is not referenced\|WARNING: cpp:member targets a"
echo"Post-processing generated html files to correct links . . ."
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.