Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Don't include "home file" in documentation search #4243

Merged
merged 1 commit into from
Nov 15, 2022

Conversation

SeanTAllen
Copy link
Member

The "home file" is only a list of the packages on the site. It ends up being extra noise in search results where it provides no value.

This commit adds front matter to the home file that will remove it from the search index when the mkdocs-material-insiders theme is removed.

The "home file" is only a list of the packages on the site. It ends
up being extra noise in search results where it provides no value.

This commit adds front matter to the home file that will remove
it from the search index when the mkdocs-material-insiders theme
is removed.
@SeanTAllen SeanTAllen requested a review from a team November 15, 2022 00:16
@ponylang-main ponylang-main added the discuss during sync Should be discussed during an upcoming sync label Nov 15, 2022
@SeanTAllen SeanTAllen added changelog - added Automatically add "Added" CHANGELOG entry on merge and removed discuss during sync Should be discussed during an upcoming sync labels Nov 15, 2022
@ponylang-main ponylang-main added the discuss during sync Should be discussed during an upcoming sync label Nov 15, 2022
@SeanTAllen SeanTAllen merged commit 2d8ac85 into main Nov 15, 2022
@SeanTAllen SeanTAllen deleted the dont-index-home-file branch November 15, 2022 19:18
@ponylang-main ponylang-main removed the discuss during sync Should be discussed during an upcoming sync label Nov 15, 2022
github-actions bot pushed a commit that referenced this pull request Nov 15, 2022
github-actions bot pushed a commit that referenced this pull request Nov 15, 2022
SeanTAllen added a commit that referenced this pull request Dec 15, 2022
I messed up implenting Don't include "home file" in documentation search.
The front matter wasn't the first thing in the file where I added it.
SeanTAllen added a commit that referenced this pull request Dec 15, 2022
I messed up implenting Don't include "home file" in documentation search.
The front matter wasn't the first thing in the file where I added it.
SeanTAllen added a commit that referenced this pull request Dec 16, 2022
I messed up implenting Don't include "home file" in documentation search.
The front matter wasn't the first thing in the file where I added it.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog - added Automatically add "Added" CHANGELOG entry on merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants