How to deploy code on a remote host: push, ssh, pull

diff --git a/pep-git.txt b/pep-git.txt
index 73b2ecbf1dccf834bd6a20252b97ed3de6922475..8aa472cd7a3ac23a6549ffdf2eb6eae732147191 100644 (file)
--- a/pep-git.txt
+++ b/pep-git.txt
@@ -283,6 +283,12 @@ non-bare repository: git refuses to update remote working directory.
 You really should push only to bare repositories. For non-bare
 repositories git prefers pull-based workflow.
 
+When you want to deploy code on a remote host and can only use push
+(because your workstation is behind a firewall and you cannot pull
+from it) you do that in two steps using two repositories: you push
+from the workstation to a bare repo on the remote host, ssh to the
+remote host and pull from the bare repo to a non-bare deployment repo.
+
 Tags
 ''''