diff --git a/doc/en/start_doc_server.sh b/doc/en/start_doc_server.sh deleted file mode 100644 index f68677409..000000000 --- a/doc/en/start_doc_server.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/usr/bin/env bash - -MY_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" -cd "${MY_DIR}"/_build/html || exit -python -m http.server 8000