diff options
| author | Pierre-Marie Pédrot | 2020-08-19 00:38:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-19 00:38:54 +0200 |
| commit | daed771ff18978dea536b277e00c0ca0149129ee (patch) | |
| tree | 98a50807d4a622c8b78ef247fe1dc391b6dbdba5 /kernel/environ.ml | |
| parent | aa926429727f1f6b5ef07c8912f2618d53f6d155 (diff) | |
| parent | 05eb5d91989c0d0c470a1b35af52c84a60853f89 (diff) | |
Merge PR #12774: Fixing tactic loc updating in #12223
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/environ.ml')
0 files changed, 0 insertions, 0 deletions