Something went wrong while fetching comments. Please try again.
Created by: jhchabran
Fixes #38754 (closed)
One could argue that all shell scripts should end in .sh but it's actually quite common in the wild to just use the shebang, so we'd better address that case for the sake of correctness.
Ran the generator locally, with a commit including changes to /dev/zoekt/update which is a shell script, but without the extension.