diff options
| author | Son Ho | 2022-11-11 15:10:57 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-11 15:26:17 +0100 |
| commit | 2ad6fec65b0d591da3a2831d4e2c7443f7a22673 (patch) | |
| tree | 093cdee9ebac0513c85cad8b7a2a6377c9d7858c | |
| parent | 411f6964f7d62de6c2b45dfb2400f76686447cd7 (diff) | |
Update the .gitignore
Diffstat (limited to '')
| -rw-r--r-- | .gitignore | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -15,6 +15,9 @@ _build/ *.byte *.native +# We group everything here +bin + # oasis generated files setup.data setup.log @@ -31,6 +34,9 @@ _opam/ # Rust working directory rust-scripts/target/ +# Generated by Nix +result + # F* .depend *.hints |