Commit Diff


commit - d72b57ac6c8914fef061e5821d4a0f58b8bb70a3
commit + 81307153727da9d10fa431813f857fd838f1aaba
blob - /dev/null
blob + 51b5ec1e61f389aa859b68c54b266ebe1e04d911 (mode 644)
--- /dev/null
+++ .github/workflows/publish.yaml
@@ -0,0 +1,35 @@
+name: Publish HTML pages
+
+on:
+  push:
+    branches: [master]
+  pull_request:
+    types: [opened, reopened, synchronize, labeled]
+  workflow_dispatch:
+
+jobs:
+  publish-doc:
+    if: |
+      github.event_name == 'push' ||
+      github.event_name == 'pull_request' &&
+      github.event.pull_request.head.repo.full_name != github.repository
+
+    runs-on: ubuntu-latest
+    steps:
+      - uses: tarantool/actions/cleanup@master
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+
+      - name: Setup mandoc
+        run: sudo apt install -y mandoc
+
+      - name: Build HTML pages
+        run: make html
+
+      - name: Publish HTML pages to GitHub Pages
+        uses: JamesIves/github-pages-deploy-action@v4.4.0
+        with:
+          folder: man3/
+        if: github.ref == 'refs/heads/master' &&
+            github.event_name != 'pull_request'