File tree Expand file tree Collapse file tree 1 file changed +2
-12
lines changed
Expand file tree Collapse file tree 1 file changed +2
-12
lines changed Original file line number Diff line number Diff line change 2828 - name : Install jq
2929 run : sudo apt-get install jq
3030
31- - name : Fetch search_original.json from docs site
32- run : curl -O https://raw.githubusercontent.com/TuringLang/docs/gh-pages/search_original.json
33-
34- - name : Convert docs site search index URLs to relative URLs
35- run : |
36- jq 'map(
37- if .href then .href = "docs/" + .href else . end |
38- if .objectID then .objectID = "docs/" + .objectID else . end)' search_original.json > fixed_docs_search.json
39-
40- - name : Merge both search index
41- run : |
42- jq -s '.[0] + .[1]' _site/search_original.json fixed_docs_search.json > _site/search.json
31+ - name : Generate augmented search index
32+ uses : TuringLang/actions/Search@main
4333
4434 - name : Deploy to GitHub Pages
4535 uses : JamesIves/github-pages-deploy-action@v4
You can’t perform that action at this time.
0 commit comments