Delete the .git/index in case it's corrupted. Do a "git reset --hard HEAD" before a git pull. Make sure a build directory cannot collide with another build directory.

db4
Doug Coleman 2010-06-13 18:23:41 -05:00
parent 9840e5e147
commit cf09a138d2
2 changed files with 14 additions and 5 deletions

View File

@ -57,6 +57,7 @@ M: unix really-delete-tree delete-tree ;
[ day>> , ]
[ hour>> , ]
[ minute>> , ]
[ drop nano-count , ]
} cleave
] { } make [ pad-00 ] map "-" join ;

View File

@ -1,9 +1,17 @@
! Copyright (C) 2008, 2010 Eduardo Cavazos, Slava Pestov.
! See http://factorcode.org/license.txt for BSD license.
USING: kernel io.launcher bootstrap.image.download
mason.common mason.platform ;
USING: bootstrap.image.download combinators.short-circuit
io.directories io.launcher kernel mason.common mason.platform ;
IN: mason.updates
: git-reset-cmd ( -- cmd )
{
"git"
"reset"
"--hard"
"HEAD"
} ;
: git-pull-cmd ( -- cmd )
{
"git"
@ -14,6 +22,8 @@ IN: mason.updates
} ;
: updates-available? ( -- ? )
".git/index" delete-file
git-reset-cmd short-running-process
git-id
git-pull-cmd short-running-process
git-id
@ -23,6 +33,4 @@ IN: mason.updates
boot-image-name maybe-download-image ;
: new-code-available? ( -- ? )
updates-available?
new-image-available?
or ;
{ [ updates-available? ] [ new-image-available? ] } 0|| ;