diff options
Diffstat (limited to 'cheri/.gitignore')
| -rw-r--r-- | cheri/.gitignore | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/cheri/.gitignore b/cheri/.gitignore new file mode 100644 index 00000000..f7f98624 --- /dev/null +++ b/cheri/.gitignore @@ -0,0 +1,5 @@ +cheri.lem +cheri_types.lem +cheriScript.sml +cheri_typesScript.sml +mips_extrasScript.sml
\ No newline at end of file |