Skip to content

Commit 2dc131d

Browse files
adding search_original.json of docs (#71)
1 parent 646205d commit 2dc131d

File tree

1 file changed

+8
-7
lines changed

1 file changed

+8
-7
lines changed

.github/workflows/publish.yml

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -27,15 +27,16 @@ jobs:
2727
- name: Install jq
2828
run: sudo apt-get install jq
2929

30-
- name: Fetch search.json from docs site
31-
run: curl -O https://raw.githubusercontent.com/TuringLang/docs/gh-pages/search.json
32-
33-
- name: Fix URLs in docs site search index
30+
- name: Fetch search_original.json from docs site
31+
run: curl -O https://raw.githubusercontent.com/TuringLang/docs/gh-pages/search_original.json
32+
33+
- name: Convert docs site search index URLs to relative URLs
3434
run: |
35-
jq 'map(if .href then .href = "docs/" + .href else . end) |
36-
map(if .objectID then .objectID = "docs/" + .objectID else . end)' search.json > fixed_docs_search.json
35+
jq 'map(
36+
if .href then .href = "docs/" + .href else . end |
37+
if .objectID then .objectID = "docs/" + .objectID else . end)' search_original.json > fixed_docs_search.json
3738
38-
- name: Merge search indices
39+
- name: Merge both search index
3940
run: |
4041
jq -s '.[0] + .[1]' _site/search_original.json fixed_docs_search.json > _site/search.json
4142

0 commit comments

Comments
 (0)