diff options
Diffstat (limited to 'otherlibs/labltk/browser/setpath.mli')
| -rw-r--r-- | otherlibs/labltk/browser/setpath.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/otherlibs/labltk/browser/setpath.mli b/otherlibs/labltk/browser/setpath.mli index f5e70090f..22bf5dc58 100644 --- a/otherlibs/labltk/browser/setpath.mli +++ b/otherlibs/labltk/browser/setpath.mli @@ -22,4 +22,4 @@ val exec_update_hooks : unit -> unit val set : dir:string -> unit val f : dir:string -> toplevel widget - (* edit the load path *) + (* edit the load path *) |