[ci] remove useless slashes

HoTT · May 24, 2023 · 7ad0850 · 7ad0850
1 parent e1da0e4
commit 7ad0850
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -59,4 +59,4 @@ jobs:
         if: ${{ github.repository_owner == 'HoTT' && github.ref == 'refs/heads/master' }}
         uses: Andrew-Chen-Wang/github-wiki-action@v4
         with:
-          path: "./_wiki_dir/"
+          path: _wiki_dir