diff options
| author | Matthieu Sozeau | 2015-10-04 14:50:45 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-06 10:01:19 +0200 |
| commit | 07f4e6b07775052cc1c5dc34cdfa7ad4eacfa94f (patch) | |
| tree | 4bb7a90d8474b038434b732fb24b9b9d69e937c3 /kernel | |
| parent | efce61af32ff1b09a21dcf88bca7d6609a0bfd27 (diff) | |
Fix bug #4354: interpret hints in the right env and sigma.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions