diff options
author | Florian Diebold <[email protected]> | 2020-02-21 22:07:29 +0000 |
---|---|---|
committer | Florian Diebold <[email protected]> | 2020-02-22 10:09:21 +0000 |
commit | c2000257941956cd4c4365d6eb6cdbc1b16e929c (patch) | |
tree | a27ef5bdc8452e89d44255cee8999df8477e136a /editors/code/src/installation | |
parent | 463df6720cc8d2c7176a48a0ca8f4e333016a16a (diff) |
Fix shift_bound_vars
It should only shift free vars (maybe the name isn't the best...)
Diffstat (limited to 'editors/code/src/installation')
0 files changed, 0 insertions, 0 deletions