diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 02:26:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-01 05:00:01 +0200 |
| commit | c403fa491bb4ef9710c6251e5d5c47c046c95e39 (patch) | |
| tree | e4b658ca6f5f34d9edffa355185fbc901ad63674 /lib/flags.ml | |
| parent | ec1e83e85543a793dc248e9d2f47dd146f9a913d (diff) | |
[nit] Qualify `Envars` use.
This eases grep to implement a different location system.
Diffstat (limited to 'lib/flags.ml')
0 files changed, 0 insertions, 0 deletions