Bug fix in automated docs deployment

MrinalJain17 · MrinalJain17 · commit b716e084fad0 · 2018-09-21T07:00:47.000+05:30
diff --git a/deploy_docs.bat b/deploy_docs.bat
@@ -6,7 +6,8 @@ cd docs
 echo Deleting old documentation...
 call make clean-cache
 rmdir files /S /Q
-git worktree remove --force
+rmdir ..\.git\worktrees\files /S /Q
+git worktree prune
 
 echo Checking out gh-pages branch into files...
 git worktree add -B gh-pages files origin/gh-pages
