From 82d599713fe82f77a27af94763815813ac91934f Mon Sep 17 00:00:00 2001 From: Shravan Goswami Date: Fri, 31 May 2024 14:18:24 +0530 Subject: [PATCH 1/2] fixed url --- .github/workflows/publish.yml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml index c0ce5d75e..4e1e4c97c 100644 --- a/.github/workflows/publish.yml +++ b/.github/workflows/publish.yml @@ -36,6 +36,9 @@ jobs: - name: Render Quarto site run: quarto render + - name: Rename original search index + run: mv _site/search.json _site/search_original.json + - name: Save _freeze folder id: cache-primes-save uses: actions/cache/save@v4 @@ -44,6 +47,23 @@ jobs: _freeze/ key: ${{ runner.os }}-primes-${{ github.run_id }} + - name: Install jq + run: sudo apt-get install jq + + - name: Fetch search_original.json from main site + run: curl -O https://raw.githubusercontent.com/TuringLang/turinglang.github.io/gh-pages/search_original.json + + - name: Convert main site search index URLs to relative URLs + run: | + jq 'map( + if .href then .href = "../" + .href else . end | + if .objectID then .objectID = "../" + .objectID else . end + )' search_original.json > fixed_main_search.json + + - name: Merge search indices + run: | + jq -s '.[0] + .[1]' _site/search_original.json fixed_main_search.json > _site/search.json + - name: Deploy to GitHub Pages uses: JamesIves/github-pages-deploy-action@v4 with: From 0dfe7eb32bfa58b36aadf5b3ec049bd35fa86b84 Mon Sep 17 00:00:00 2001 From: Shravan Goswami Date: Fri, 31 May 2024 14:42:42 +0530 Subject: [PATCH 2/2] search workflow done --- .github/workflows/publish.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml index 4e1e4c97c..c4b34db55 100644 --- a/.github/workflows/publish.yml +++ b/.github/workflows/publish.yml @@ -57,10 +57,9 @@ jobs: run: | jq 'map( if .href then .href = "../" + .href else . end | - if .objectID then .objectID = "../" + .objectID else . end - )' search_original.json > fixed_main_search.json + if .objectID then .objectID = "../" + .objectID else . end)' search_original.json > fixed_main_search.json - - name: Merge search indices + - name: Merge both search index run: | jq -s '.[0] + .[1]' _site/search_original.json fixed_main_search.json > _site/search.json