New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Timer osx pr #3998
Timer osx pr #3998
Conversation
I still use os x 10.10 and GHC 7.8.4! |
Cunning! (don't take this as a code reivew, I don't know this stuff well enough) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice hack!
echo "$* took $duration seconds." | ||
echo "whole job took $total_duration seconds so far." | ||
|
||
# Terminate on OSX |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would be nice to mention that we're doing this to populate the cache.
Evil. :) But I ran out of disk space even when I just tried a simplified version of the build; let us see if the same problem shows up here. |
|
||
# Terminate on OSX | ||
if [ $total_duration -ge 2400 -a $(uname) = "Darwin" ]; then | ||
echo "Job taking over 40 minutes. Terminating" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, it would be good if this told the person to rerun the build.
if osx build is too slow, it will cut it down, making the cache populate. So restarting the job would help!