From 895b777b724a05b71ee87abc13d43aa5d8b8771f Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 14 May 2024 13:33:51 +0200
Subject: [PATCH] feat(ci): add action to sync with hacspec.github.io

---
 .github/workflows/push_readme.yml | 37 +++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 .github/workflows/push_readme.yml

diff --git a/.github/workflows/push_readme.yml b/.github/workflows/push_readme.yml
new file mode 100644
index 000000000..0066a2adb
--- /dev/null
+++ b/.github/workflows/push_readme.yml
@@ -0,0 +1,37 @@
+name: Push `README.md`
+
+on:
+  push:
+    branches: [main]
+    
+jobs:
+  push_readme:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        path: hax
+    - uses: actions/checkout@v4
+      with:
+        repository: "hacspec/hacspec.github.io"
+        path: website
+        token: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}}
+    - name: Publish documentation
+      run: |
+        (
+          README_ORIGINAL="https://github.com/hacspec/hax/blob/main/README.md"
+          echo "<!-- WARNING: a GitHub action periodically replaces this file with ${README_ORIGINAL}. Do not make any modification to this file, instead make a PR to ${README_ORIGINAL} -->"
+          echo ""
+          cat hax/README.md
+        ) > website/README.md
+        cd website
+        # Replace the `🌐 Website` link to a GitHub link
+        sed -i 's#.*🌐 Website.*#  <a href="https://github.com/hacspec/hax">🔗 GitHub</a> |#' README.md
+        git config --local user.name "github-actions[bot]"
+        git config --local user.email "41898282+github-actions[bot]@users.noreply.github.com"
+        git add -A
+        git commit -m "Readme update" \
+          && git push https://$USERNAME:$PUSH_HACSPEC_GITHUB_TOKEN@github.com/hacspec/hacspec.github.io
+      env:
+        PUSH_HACSPEC_GITHUB_TOKEN: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}}
+        USERNAME: github-actions[bot]