diff options
| author | Sverker Eriksson <[email protected]> | 2018-07-18 15:02:36 +0200 |
|---|---|---|
| committer | Sverker Eriksson <[email protected]> | 2018-07-18 15:02:36 +0200 |
| commit | 866b073857f31a04561b96bf666cb9e6eacf0cfd (patch) | |
| tree | 8bb16a8ed90938d5e73f321f50a1b2710695c582 /erts/etc/unix | |
| parent | 79cfc7493996dea4a7eed5c84421b45212d80edf (diff) | |
| parent | 6a98a4b05ae77739d27f2a9fb018786906e6918c (diff) | |
| download | otp-866b073857f31a04561b96bf666cb9e6eacf0cfd.tar.gz otp-866b073857f31a04561b96bf666cb9e6eacf0cfd.tar.bz2 otp-866b073857f31a04561b96bf666cb9e6eacf0cfd.zip | |
Merge branch 'maint'
Diffstat (limited to 'erts/etc/unix')
| -rw-r--r-- | erts/etc/unix/cerl.src | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/erts/etc/unix/cerl.src b/erts/etc/unix/cerl.src index 896e4c8e45..2e034513b0 100644 --- a/erts/etc/unix/cerl.src +++ b/erts/etc/unix/cerl.src @@ -264,13 +264,14 @@ if [ "x$GDB" = "x" ]; then valversion=`valgrind --version` valmajor=`echo $valversion | sed 's,[a-z]*\-\([0-9]*\).*,\1,'` valminor=`echo $valversion | sed 's,[a-z]*\-[0-9]*.\([0-9]*\).*,\1,'` + valint=`echo "$valmajor * 1000 + $valminor" | bc` if [ "x$VALGRIND_LOG_XML" = "x" ]; then valgrind_xml= log_file_prefix="--log-file=" else export VALGRIND_LOG_XML valgrind_xml="--xml=yes" - if [ $valmajor -gt 2 -a $valminor -gt 4 ]; then + if [ $valint -gt 3004 ]; then log_file_prefix="--xml-file=" else log_file_prefix="--log-file=" @@ -279,7 +280,7 @@ if [ "x$GDB" = "x" ]; then if [ "x$VALGRIND_LOG_DIR" = "x" ]; then valgrind_log= else - if [ $valmajor -gt 2 -a $valminor -gt 4 ]; then + if [ $valint -gt 3004 ]; then valgrind_log="$log_file_prefix$VALGRIND_LOG_DIR/$VALGRIND_LOGFILE_PREFIX$VALGRIND_LOGFILE_INFIX$EMU_NAME.log.$$" else valgrind_log="$log_file_prefix$VALGRIND_LOG_DIR/$VALGRIND_LOGFILE_PREFIX$VALGRIND_LOGFILE_INFIX$EMU_NAME.log" |