From 521f346b6f6c1d23116dc30ed9470775e3d47ffb Mon Sep 17 00:00:00 2001 From: Evan Burkey Date: Wed, 3 May 2023 14:29:03 -0700 Subject: [PATCH] remove redundant script --- docs.sh | 6 ------ 1 file changed, 6 deletions(-) delete mode 100755 docs.sh 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/