diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/.gitignore | 1 | ||||
| -rw-r--r-- | tools/addentry.ml | 2 | ||||
| -rw-r--r-- | tools/addpaper.ml | 2 |
3 files changed, 3 insertions, 2 deletions
diff --git a/tools/.gitignore b/tools/.gitignore new file mode 100644 index 0000000..261b053 --- /dev/null +++ b/tools/.gitignore @@ -0,0 +1 @@ +*.cmo diff --git a/tools/addentry.ml b/tools/addentry.ml index 21f5d6f..a00dd28 100644 --- a/tools/addentry.ml +++ b/tools/addentry.ml @@ -34,4 +34,4 @@ let () = else ( printf "addentry: Add paper Makefile entry.\n"; printf "addentry: usage: <file_index> <paper_name_index>\n" - )
\ No newline at end of file + );; diff --git a/tools/addpaper.ml b/tools/addpaper.ml index 457524e..1e281a3 100644 --- a/tools/addpaper.ml +++ b/tools/addpaper.ml @@ -56,4 +56,4 @@ let () = if Array.length Sys.argv >= 5 then else ( printf "addpaper: Creates papers for TeX.\n"; printf "addpaper: usage: <file_name> <document_title>\n" - ); + );; |