diff options
Diffstat (limited to 'debugger/parameters.ml')
| -rw-r--r-- | debugger/parameters.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/debugger/parameters.ml b/debugger/parameters.ml index 67078b2fc..9d518e549 100644 --- a/debugger/parameters.ml +++ b/debugger/parameters.ml @@ -17,7 +17,7 @@ open Primitives open Config -open Misc +open Debugger_config let program_loaded = ref false let program_name = ref "" @@ -31,5 +31,9 @@ let add_path dir = load_path := dir :: except dir !load_path; Envaux.reset_cache() +let add_path_for mdl dir = + let old = try Hashtbl.find load_path_for mdl with Not_found -> [] in + Hashtbl.replace load_path_for mdl (dir :: old) + (* Used by emacs ? *) let emacs = ref false |