diff options
| author | Em Zhan | 2023-07-09 17:20:38 +0000 |
|---|---|---|
| committer | GitHub | 2023-07-09 17:20:38 +0000 |
| commit | 9a324f337a2705e68035a356ad6b626ee4c6669b (patch) | |
| tree | cceca85e3bf0ec7860e4873e6e103fc449b07ca9 /.ignore | |
| parent | 7c338429f845315fb276ff482f91b94b3102dbd8 (diff) | |
docs: Update mdBook theme and improve maintainability (#7524)
Diffstat (limited to '.ignore')
| -rw-r--r-- | .ignore | 3 |
1 files changed, 0 insertions, 3 deletions
@@ -1,5 +1,2 @@ # Things that we don't want ripgrep to search that we do want in git # https://github.com/BurntSushi/ripgrep/blob/master/GUIDE.md#automatic-filtering - -# Minified JS vendored from mdbook -book/theme/highlight.js |