aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-06 11:32:31 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-06 11:32:31 +0100
commit8b5d02d8706f99015c2ce8efcad32b7af228dd53 (patch)
treeab46e3eb533ad5655b77d164b12b778f05b34131
parent23cbf43f353c50fa72b72d694611c5c14367cea2 (diff)
Prevent coq_makefile from parsing project files in the reverse order. (Fix bug #4477)
The bug was a bit subtle. Function process_cmd_line can be called in three different ways: 1. tail-recursively to accumulate parsed options in reverse order, 2. directly to parse a file (coqide) or a command line (coq_makefile), 3. recursively to handle a "-f" option. Once its execution finished, the function reversed its accumulator so that the parsed options are in correct order. Due to the third case, this means that the final local order of options was depending on the parity of the depth of "-f" options. This commit fixes it by changing the function so that the recursive call gets the actual accumulator rather than its reversed version. Warning: this will break all the projects that were inadvertently (or not) relying on the bug. This might also require a further commit if coq_makefile itself was relying on the bug.
-rw-r--r--ide/project_file.ml46
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 152f76cc0..07ab5344d 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -48,7 +48,7 @@ let parse f =
res
let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function
- | [] -> opts,List.rev l
+ | [] -> opts, l
| ("-h"|"--help") :: _ ->
raise Parsing_error
| ("-no-opt"|"-byte") :: r ->
@@ -128,6 +128,10 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
else if (Filename.check_suffix f ".mlpack") then MLPACK f
else Subdir f) :: l) r
+let process_cmd_line orig_dir opts l args =
+ let (opts, l) = process_cmd_line orig_dir opts l args in
+ opts, List.rev l
+
let rec post_canonize f =
if Filename.basename f = Filename.current_dir_name
then let dir = Filename.dirname f in