1 files changed, 0 insertions, 15 deletions
diff --git a/dist/man.sh b/dist/man.sh
deleted file mode 100755
index 4c5316ddb..000000000
--- a/dist/man.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-#! /bin/bash
-
-cd $(dirname $0)/..
-
-rm -rf doc/_build/man/*
-
-set -e
-
-docker run --rm -it \
-  -v /$(pwd):/src \
-  -w //src/doc \
-  btdi/sphinx:featured \
-  sh -c "sphinx-build -T -b man . ./_build/man"
-
-nroff -man doc/_build/man/ghdl.1