Skip to content

Commit

Permalink
PullReps: merge local main, instead of remote main
Browse files Browse the repository at this point in the history
  • Loading branch information
SunSerega committed Apr 3, 2024
1 parent fdcce99 commit 82985e9
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions DataScraping/Reps/PullReps.pas
Original file line number Diff line number Diff line change
Expand Up @@ -62,12 +62,15 @@ procedure PullRep(name, branch, nick: string);

ExecCommands(path, nick, nil
, $'echo [checkout] && git checkout {branch} 2>&1'
, $'echo [pull] && git pull {remote_official} main & echo [pull-own]: && git pull {remote_own} {branch}'
, $'echo [pull-own]: && git pull {remote_own} {branch}'
, $'echo [fetch] && git fetch {remote_official} main:main'
, $'echo [pull] && git merge main'
);

if not disable_push then
ExecCommands(path, nick, |'console only'|
, $'echo [push] && git push {remote_own} {branch} || cd .'
, $'echo [push main] && git push {remote_own} main || cd .'
, $'echo [push {branch}] && git push {remote_own} {branch} || cd .'
);

Otp($'Done pulling {nick}');
Expand Down

0 comments on commit 82985e9

Please sign in to comment.