aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-26 12:34:24 +0200
committerEmilio Jesus Gallego Arias2018-11-24 20:47:12 +0100
commit8f9dcb8418ac4db5cf3e4302f61d543d0c47cbdf (patch)
tree7c3722763bf495b56b6245640ab3d89b72f21a45 /dev/ci
parente0f55aecee2ed9fc6f56979c255688e08b136c20 (diff)
[toplevel] Allow to specify default options.
In some cases, toplevel ML clients may want to modify the default set of flags that is passed to the main initalization routine. This is for example useful for `idetop` to suppress some undesired printing at startup. I would say that clients ought to have more control, but I do expect that PRs such as #8690 will help providing a better separation thus a mode orthogonal API.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions