diff options
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index dac88a4733..1bf393fd08 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -80,8 +80,8 @@ let is_unsafe s = Stringset.mem s !unsafe_set let boxed_definitions = ref true let set_boxed_definitions b = boxed_definitions := b -let boxed_definitions _ = !boxed_definitions - +let boxed_definitions _ = !boxed_definitions + (* Flags for external tools *) let subst_command_placeholder s t = |