diff --git a/docs.sh b/docs.sh deleted file mode 100755 index eebe093..0000000 --- a/docs.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/usr/bin/env bash - -mkdocs build -ssh debian@fputs.com rm -rf /var/www/fputs.com/docs/libflint -ssh debian@fputs.com mkdir -p /var/www/fputs.com/docs/libflint -scp -r site/* debian@fputs.com:/var/www/fputs.com/docs/libflint/