Changes in contrib/tools/random_check.sh [1b20da0:a35b458] in mainline

File:

• contrib/tools/random_check.sh (modified) (5 diffs)

contrib/tools/random_check.sh

@@ -88 +88 @@
         COUNTER=$(( $COUNTER + 1 ))
         echo "Try #$COUNTER ($FAILED failed):" >&2
-        
+
         (
                 echo "  Cleaning after previous build." >&2
                 make distclean -j$JOBS 2>&1 || exit 1
-                
-                
+
+
                 echo "  Preparing random configuration." >&2
                 # It would be nicer to allow set the constraints directly to
@@ -105 +105 @@
                                 exit 2
                         fi
-                        
+
                         make random-config 2>&1 || exit 1
-                        
+
                         tr -d ' ' <Makefile.config >"${FILENAME_PREFIX}config.trimmed"
-                        
+
                         THIS_CONFIG_OKAY=true
                         while read pattern; do
@@ -117 +117 @@
                                 fi
                         done <"$PRUNE_CONFIG_FILE"
-                        
+
                         rm -f "${FILENAME_PREFIX}config.trimmed"
-                        
+
                         if $THIS_CONFIG_OKAY; then
                                 break
                         fi
                 done
-                
-                
+
+
                 # Report basic info about the configuration and build it
                 BASIC_CONFIG=`sed -n \
@@ -134 +134 @@
                         | paste '-sd,' | sed 's#,#, #g'`
                 echo -n "  Building ($BASIC_CONFIG)... " >&2
-        
+
                 make -j$JOBS 2>&1
                 if [ $? -eq 0 ]; then
@@ -143 +143 @@
                         exit 1
                 fi
-                
+
         ) >random_run_$COUNTER.log
         RC=$?
-        
+
         if [ $RC -ne 0 ]; then
                 tail -n 10 random_run_$COUNTER.log | sed 's#.*#    | &#'
                 FAILED=$(( $FAILED + 1 ))
         fi
-        
+
         if [ -e Makefile.config ]; then
                 cp Makefile.config "$FILENAME_PREFIX$COUNTER.Makefile.config"