From c471b382f5f8e060adcaca092ad3b676634e9025 Mon Sep 17 00:00:00 2001
From: Xinbin Huang <bin.huangxb@gmail.com>
Date: Mon, 8 Jun 2020 21:01:11 -0700
Subject: [PATCH] Remove start_doc_server.sh script

---
 doc/en/start_doc_server.sh | 5 -----
 1 file changed, 5 deletions(-)
 delete mode 100644 doc/en/start_doc_server.sh

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