diff options
| author | Théo Zimmermann | 2019-03-18 21:05:30 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-18 21:05:30 +0100 |
| commit | 238d83080c8dbed458b026c93f5c723c1bd7c937 (patch) | |
| tree | f990ec517483b1d80821538554c8a29607a0cceb /configure.ml | |
| parent | 9ac5483132b42e845a0708491843693b70893eef (diff) | |
| parent | 0c3aa2f4bbd0bb5124ff3cc95759cb7cb89caa6b (diff) | |
Merge PR #9777: [Nix] A few improvements
Reviewed-by: Zimmi48
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions