diff options
| author | Emilio Jesus Gallego Arias | 2019-07-31 21:07:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-31 21:11:20 +0200 |
| commit | 9b7816a80c77d7f9b4cea35f8ed983763bd8a5c7 (patch) | |
| tree | 40cf3f202cebd32a7a4ef200487425a60ad7cc42 /doc/plugin_tutorial/Makefile | |
| parent | 4e679df3c15e5e554ff9ef85138f9c55396e9f0b (diff) | |
[toplevel] Make all argument lists to be in user-declared order.
As reported by Karl Palmskog, some lists of arguments were supposed to
appear in reverse order whereas others do appear in the natural order
they are declared.
Given that in some cases, such as require, order is quite important,
we make the parsing return lists in the right order so clients don't
have to care about doing `List.rev`.
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions
