diff options
| author | Pierre-Marie Pédrot | 2019-05-17 14:18:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-20 14:11:44 +0200 |
| commit | e69e4f7fd9aaba0e3fd6c38624e3fdb0bd96026c (patch) | |
| tree | caf9be18ce8da31926142946455fa7982f9d84fd /kernel/environ.ml | |
| parent | 27468ae02bbbf018743d53a9db49efa34b6d6a3e (diff) | |
Do not perform the section variable check on global recipes.
By construction, we know that Cooking is returning the right set of
used variables. This set has been checked already once at the time
when the definition was performed inside the section.
Diffstat (limited to 'kernel/environ.ml')
0 files changed, 0 insertions, 0 deletions