home: ssh: add 'work' host

2022-01-25 15:46:17 +01:00 · 2022-01-25 15:46:17 +01:00 · ef875f881f
parent b33cefde63
commit ef875f881f
2 changed files with 10 additions and 0 deletions
--- a/home/git/default.ignore
+++ b/home/git/default.ignore
@ -24,3 +24,7 @@ compile_commands.json
 # Swap and backup files
 *~
 ~.swp
+
+# Direnv files
+.envrc
+.direnv/
--- a/home/ssh/default.nix
+++ b/home/ssh/default.nix
@ -40,6 +40,12 @@ in
        identityFile = "~/.ssh/shared_rsa";
        user = "ambroisie";
      };
+
+      work = {
+        hostname = "workspaces.dgexsol.fr";
+        identityFile = "~/.ssh/shared_rsa";
+        user = "bruno_belanyi";
+      };
    };

    extraConfig = ''