diff --git a/collects/planet2/scribblings/planet2.scrbl b/collects/planet2/scribblings/planet2.scrbl index f3981421f3..55a684dfd8 100644 --- a/collects/planet2/scribblings/planet2.scrbl +++ b/collects/planet2/scribblings/planet2.scrbl @@ -280,7 +280,7 @@ Then initialize the Git repository locally and do your first push: @commandline{git add *} @commandline{git commit -m "First commit"} @commandline{git remote add origin https://github.com//.git} -@commandline{git push origin master} +@commandline{git push -u origin master} Now, publish your package source as: