diff options
author | Griffin Smith <grfn@gws.fyi> | 2021-09-23T13·45-0400 |
---|---|---|
committer | grfn <grfn@gws.fyi> | 2021-09-27T14·55+0000 |
commit | f746020d5891294e42d6001041a78a6b77f50783 (patch) | |
tree | 80fd10ae9f5fb2628da30b2b79442ae3a2d901ce /.rgignore | |
parent | f762711b8171c86f9a9ebfb1a9a5c3eda11b0862 (diff) |
fix(gs/emacs): Disable idris temporarily r/2922
This doesn't work right now, and I'm not currently writing any idris Change-Id: I7c090ad9f05c5d24f4f80fdd444e8995629aaba4 Reviewed-on: https://cl.tvl.fyi/c/depot/+/3641 Tested-by: BuildkiteCI Reviewed-by: grfn <grfn@gws.fyi>
Diffstat (limited to '.rgignore')
0 files changed, 0 insertions, 0 deletions