diff options
author | 2017-08-31 17:40:28 +0200 | |
---|---|---|
committer | 2018-07-03 13:39:18 +0200 | |
commit | 6ba75b01a7e39f48a325b04fd891939927b981da (patch) | |
tree | 3725d6f85e58a5d5b5707607ca3727030fd87434 /ide | |
parent | c11bd7b181d6e53910dc8d39c5360f35c7b24674 (diff) |
Term_typing: remove unused argument to internal function.
The function is defined with a typo but called with the same env that
is mistakenly not shadowed.
An alternative to this commit would be to fix the typo.
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions