diff --git a/tools/publish b/tools/publish index a08b405b..51b519b5 100755 --- a/tools/publish +++ b/tools/publish @@ -20,5 +20,15 @@ then mkdocs build fi +# Generate robots.txt +cat > site/robots.txt <