diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 11:32:31 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 11:32:31 +0100 |
commit | 8b5d02d8706f99015c2ce8efcad32b7af228dd53 (patch) | |
tree | ab46e3eb533ad5655b77d164b12b778f05b34131 /plugins/firstorder | |
parent | 23cbf43f353c50fa72b72d694611c5c14367cea2 (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.
Diffstat (limited to 'plugins/firstorder')
0 files changed, 0 insertions, 0 deletions