diff options
Diffstat (limited to 'debugger/debugger_config.mli')
| -rw-r--r-- | debugger/debugger_config.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debugger/debugger_config.mli b/debugger/debugger_config.mli index f725acecf8..ab935d9324 100644 --- a/debugger/debugger_config.mli +++ b/debugger/debugger_config.mli @@ -34,4 +34,4 @@ val make_checkpoints : bool ref (*** Environment variables for debugee. ***) -val environment : string list ref +val environment : (string * string) list ref |