Hi, I have found a work-a-round that works for me: I patched the package.json of sourcegraph.sourcegraph and set “extensionKind”: [ “ui” ], and then reinstalled the extension.
When I now establish a remote connection, Sourcegraph code search works fine with the local settings also in the remote workspace.
I see no reason why the extension should be installed on the remote host at all. Maybe extensionKind:[ui] would be a good default setting for the next release?