doc: Update the guide on deploying dev site

`docs/` should be removed from .gitignore before making a commit, because otherwise the external links (e.g., plat-doc/islet_rmm) will be inaccessible. Signed-off-by: Changho Choi <ch754.choi@samsung.com>
islet-project · Oct 16, 2024 · 9338ccb · 9338ccb
1 parent 2dd75a1
commit 9338ccb
Showing 1 changed file with 7 additions and 2 deletions.
diff --git a/doc/dev-site.md b/doc/dev-site.md
@@ -16,13 +16,18 @@ $ git rebase main
 $ ./scripts/make_doc.sh
 ```
 
-### 4. Commit the result docs
+### 4. Remove the line containing `docs/` in .gitignore temporarily
+```sh
+$ grep -v 'docs/' .gitignore > tmp.txt && mv tmp.txt .gitignore
+```
+
+### 5. Commit the result docs
 ```sh
 $ git add docs/*
 $ git commit -s -m "Bump to latest main branch"
 ```
 
-### 5. Deploy the docs to the remote site
+### 6. Deploy the docs to the remote site
 ```sh
 $ git push origin gh-pages --force
 ```