diff --git a/base/user_setup.sh b/base/user_setup.sh index 651feb507e69402b73e963de560e814ea9d4a53f..263cab4c655351171d5893e736f917537f4849b7 100644 --- a/base/user_setup.sh +++ b/base/user_setup.sh @@ -1,4 +1,8 @@ # user setup script + +# Disable core dumps +ulimit -c 0 + # set git config if [ ! "$(git config --get user.name)" ] then