diff --git a/generator/params.ml b/generator/params.ml new file mode 100644 index 0000000000000000000000000000000000000000..852731d4c2d03b7399ee0685fdf164bfe88568aa --- /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