diff options
| author | Pierre Boutillier | 2014-07-21 15:52:19 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-07-22 18:21:58 +0200 |
| commit | 34b0bde46bd46ab4c467caccc7a6aebb5a999a74 (patch) | |
| tree | aca142bd1408d03ee6bf09aef8462e26e43cadb3 /ide/ideutils.ml | |
| parent | 82f63ddf9c7d2fdd670f292f725a4295655db193 (diff) | |
Ide: Drop argument added by MacOS during .app launch
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 424c41a602..945e425c6c 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -253,11 +253,6 @@ let coqtop_path () = with Not_found -> "coqtop" in file -let rec print_list print fmt = function - | [] -> () - | [x] -> print fmt x - | x :: r -> print fmt x; print_list print fmt r - (* In win32, when a command-line is to be executed via cmd.exe (i.e. Sys.command, Unix.open_process, ...), it cannot contain several quoted "..." zones otherwise some quotes are lost. Solution: we re-quote |