From 14a2b55b06a46e7d63ba1f3b34dc039fc3be8f30 Mon Sep 17 00:00:00 2001 From: Alan Schmitt <alan.schmitt@polytechnique.org> Date: Wed, 25 Nov 2015 18:20:20 +0100 Subject: [PATCH] forgot a file --- generator/params.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 generator/params.ml diff --git a/generator/params.ml b/generator/params.ml new file mode 100644 index 0000000..852731d --- /dev/null +++ b/generator/params.ml @@ -0,0 +1,12 @@ +let debug = ref false +let logging = ref false + +(****************************************************************) +(* MODES *) + +type generate_mode = + | Mode_unlogged + | Mode_line_token + | Mode_logged + +let current_mode = ref Mode_unlogged -- GitLab