Merge branch 'master' into perso

Conflicts:
	.ssh/config

diff --git a/.ssh/config b/.ssh/config
index 352745df114de71bf52b52393ad4f76df3bd3cdc..8374f13eb4397f46adc9a093133cea4539820673 100644 (file)
--- a/.ssh/config
+++ b/.ssh/config
@@ -1009,6 +1009,8 @@ Host info21 infossh ssh.dptinfo ssh.dptinfo.ens-cachan.fr
     User vlegalli
     ForwardAgent yes
 
+# Le ! permet de ne pas capturer ssh.dptinfo dans *.dptinfo
+# Sinon on crée une boucle
 Host *.dptinfo !ssh.dptinfo
     HostName %h.ens-cachan.fr
     User vlegalli