mason.git: rename git-pull to git-clone-or-pull since that's what it does.
parent
a7958c65b2
commit
43b5eab7a4
|
@ -86,7 +86,7 @@ IN: mason.git
|
|||
|
||||
PRIVATE>
|
||||
|
||||
: git-pull ( -- id )
|
||||
: git-clone-or-pull ( -- id )
|
||||
#! Must be run from builds-dir.
|
||||
"factor" exists? [
|
||||
check-repository [
|
||||
|
|
|
@ -24,7 +24,7 @@ SYMBOLS: latest-sources last-built-sources ;
|
|||
|
||||
: update-sources ( -- )
|
||||
#! Must be run from builds-dir
|
||||
git-pull latest-boot-image latest-counter <sources>
|
||||
git-clone-or-pull latest-boot-image latest-counter <sources>
|
||||
latest-sources set-global ;
|
||||
|
||||
: should-build? ( -- ? )
|
||||
|
|
Loading…
Reference in New Issue