On 2023-05-10 05:49:19 +0100, Tim Woodall wrote: > On Tue, 9 May 2023, William Torrez Corea wrote: > > > Command: > > > > git push master origin > > > > > shouldn't that be git push origin master? Or even origin main?
Or in general, simply "git push", since the current branch and the associated upstream branch are the default. -- Vincent Lefèvre <vinc...@vinc17.net> - Web: <https://www.vinc17.net/> 100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/> Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)
