diff options
Diffstat (limited to 'debugger/parameters.mli')
| -rw-r--r-- | debugger/parameters.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/debugger/parameters.mli b/debugger/parameters.mli index 244d24b35f..44c850d5c7 100644 --- a/debugger/parameters.mli +++ b/debugger/parameters.mli @@ -23,3 +23,5 @@ val add_path_for : string -> string -> unit (* Used by emacs ? *) val emacs : bool ref + +val machine_readable : bool ref |