summaryrefslogtreecommitdiff
path: root/bin
diff options
context:
space:
mode:
authorMarius Peter <marius.peter@tutanota.com>2025-07-20 18:00:04 +0200
committerMarius Peter <marius.peter@tutanota.com>2025-07-20 18:00:04 +0200
commit75baea720c97f73370786b95006a65da7762264b (patch)
tree45fe1b841774cf145ef449aecb3acc12f16f4632 /bin
parent395bdf4668e37e98ff33151aa44426afe0e20e75 (diff)
Miscellaneous cleanup.
Diffstat (limited to 'bin')
-rw-r--r--bin/main.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/bin/main.ml b/bin/main.ml
index 2b3d552..fdc8baf 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1 +1,3 @@
+(* -*- mode: tuareg; -*- *)
+
let () = Ogit.Main.run ()
Copyright 2019--2025 Marius PETER