From f5b9e0276674b153a213509fb2db8d8d79e0aebc Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Thu, 7 Apr 2022 00:44:49 +0100
Subject: [PATCH] modify deploy_docs to not need relative path

---
 deploy_docs.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/deploy_docs.sh b/deploy_docs.sh
index 2f77858..d9d89bc 100755
--- a/deploy_docs.sh
+++ b/deploy_docs.sh
@@ -23,7 +23,7 @@ fi
 
 # generate the docs
 cd $1
-../$2/build/bin/doc-gen4 /mathlib4_docs/ Mathlib
+../$2/build/bin/doc-gen4 Mathlib
 
 if [ "$3" = "true" ]; then
   cd ..