diff options
| author | Charlie Groves | 2022-08-03 14:00:39 +0000 |
|---|---|---|
| committer | GitHub | 2022-08-03 14:00:39 +0000 |
| commit | c5f8a835f54b27c9f1c22c8321378a309d371309 (patch) | |
| tree | 920a0196978f66c535bc6c4573b1d8110dc79418 | |
| parent | 6e7774bb79a7a470df5ebbc45f2694f479e673ab (diff) | |
Add a .ignore file to make ripgrep more useful (#3315)
Co-authored-by: Michael Davis <mcarsondavis@gmail.com>
| -rw-r--r-- | .ignore | 5 |
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 |