Unnamed repository; edit this file 'description' to name the repository.
Add a .ignore file to make ripgrep more useful (#3315)
Co-authored-by: Michael Davis <[email protected]>
Charlie Groves 2022-08-03
parent 6e7774b · commit c5f8a83
-rw-r--r--.ignore5
1 files changed, 5 insertions, 0 deletions
diff --git a/.ignore b/.ignore
new file mode 100644
index 00000000..865856b4
--- /dev/null
+++ b/.ignore
@@ -0,0 +1,5 @@
+# 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