summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorRobert Norton2018-07-09 16:30:06 +0100
committerRobert Norton2018-07-09 16:30:13 +0100
commit936f1beb2bbc9db6182ba8b706668e146c3657d9 (patch)
tree1bc2a4852b45e4cdd9e3c738c33283b460f5fc3d /lib
parent6c04e4bf31b7632283c69a30c30f3869e9146874 (diff)
Changes for anonymisation. Ensure headers are in correct format. Remove some redundant files.
Diffstat (limited to 'lib')
-rw-r--r--lib/main.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/main.ml b/lib/main.ml
index e9dcb4e0..c1b6fcae 100644
--- a/lib/main.ml
+++ b/lib/main.ml
@@ -1,4 +1,3 @@
-
(**************************************************************************)
(* Sail *)
(* *)