diff options
| author | Emilio Jesus Gallego Arias | 2017-09-20 08:30:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-09-20 08:30:24 +0200 |
| commit | fb482f6b02156c1fcf029263083b0371e030a2cd (patch) | |
| tree | 99f3ee49f015b2859f627cf2e57db0eb5ef3cb27 /API | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
[flags] Flag `open Flags`
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions