From: Makarius <makarius@sketis.net>
* System *
- SSH connections allow both bash and zsh as remote shell. This is
particularly important for macOS, where zsh is the default user shell.
This refers to Isabelle/4fbdef3e2a55.
Makarius
Last updated: Dec 10 2025 at 12:50 UTC