Hi! I want to use two machines over ssh. One machine has a differnt port than 22. But I can't set a port in the host specifications for ssh. Is there any way to do so? Maybe I could use DISTCC_SSH with a script, but I think thats not a _real_ solution. Cheers, Steffen