Profils

Shells locaux, connexions SSH et ports série, rangés par groupes.

Le gestionnaire de profils

Ouvrez-le depuis la flèche ▾ de la barre d’onglets › Gérer les profils…, ou depuis la palette. La liste est classée par groupe et filtrable. Le + crée un profil Shell local, SSH ou Port série.

Chaque profil a un nom, un groupe, une icône et une couleur, reprise par ses onglets. L’un d’eux est le profil par défaut, ouvert par le + et par Ctrl+Shift+T.

Shell local

• Exécutable et arguments (par exemple pwsh.exe -NoLogo, bash --login -i) ;
• dossier de travail (par défaut, votre dossier personnel) ;
• variables d’environnement, une par ligne (NOM=valeur) ;
• intégration shell, activée par défaut : elle permet l’historique et les suggestions (voir Suggestions et coloration).

Les profils détectés au démarrage sont mis à jour automatiquement. Un shell désinstallé reste dans la liste, marqué « introuvable ».

Importer ~/.ssh/config

Le bouton Importer ~/.ssh/config du gestionnaire reprend vos hôtes (Host, HostName, User, Port, IdentityFile, ProxyJump). Un écran de prévisualisation montre les profils qui seront créés dans le groupe « ~/.ssh/config ».

Supprimer un profil

La suppression demande une confirmation. Les onglets déjà ouverts avec ce profil restent ouverts.