Closed podsvirov closed 5 months ago
Ping.
Hi. Thanks for your contribution, and your patience! This looks good - I expect to merge (*) it shortly.
(* actually rebase)
Now in master as commit https://github.com/google/jsonnet/commit/a4aeb1d05c6e63cfe219d76c83f4174d7903313e
Looks like GitHub's detection of merges didn't realise it is from this PR though, so I'll close this manually.
Ping.