*** 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