diff --git a/Makefile b/Makefile deleted file mode 100644 index aa76b509654e..000000000000 --- a/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -.PHONY: docs - -docs: - @if [ ! -x "./scripts/serve_docs" ]; then \ - echo "Error: The 'serve_docs' script is not executable."; \ - echo "Please make it executable by running:"; \ - echo " chmod +x \"./scripts/serve_docs\""; \ - echo "Then, run 'make docs' again."; \ - exit 1; \ - fi - @./scripts/serve_docs \ No newline at end of file