diff --git a/generate_docs.sh b/generate_docs.sh new file mode 100755 index 0000000000000000000000000000000000000000..111ee2f7762b5dd6fd5cebdda76e703d509b5618 --- /dev/null +++ b/generate_docs.sh @@ -0,0 +1,18 @@ +#!/bin/bash + +# Script to generate the docs +NAME_CURRENT_FILE="`realpath \"$0\"`" +DIRNAME_CURRENT_FILE=$(dirname $NAME_CURRENT_FILE) +DOCS_DIR="$DIRNAME_CURRENT_FILE/docs/" + + +# echo "$NAME_CURRENT_FILE" +# echo "$DIRNAME_CURRENT_FILE" +# echo "$DOCS_DIR" + +# Generate docs +echo "Generating documentation" +cd $DOCS_DIR +make clean +make html +echo "Done" \ No newline at end of file