# HG changeset patch
# User wenzelm
# Date 1615307511 -3600
# Node ID e488f4bb1c79b2655359c505d03bffe099327cf7
# Parent  48569c862eb8db340c090ef28c9385f82beeb2e1
obsolete (see 0c837beeb5e7);

diff -r 48569c862eb8 -r e488f4bb1c79 lib/scripts/timestart.bash
--- a/lib/scripts/timestart.bash	Tue Mar 09 17:15:21 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Author: Makarius
-#
-# timestart - setup bash environment for timing.
-#
-
-TIMES_RESULT=""
-
-function get_times () {
-  local TMP="${TMPDIR:-/tmp}/get_times$$"
-  times > "$TMP"   # No pipe here!
-  TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | perl -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
-  rm -f "$TMP"
-}
-
-get_times  # sets TIMES_RESULT
diff -r 48569c862eb8 -r e488f4bb1c79 lib/scripts/timestop.bash
--- a/lib/scripts/timestop.bash	Tue Mar 09 17:15:21 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Author: Makarius
-#
-# timestop - report timing based on environment (cf. timestart.bash)
-#
-
-TIMES_REPORT=""
-
-function show_times ()
-{
-  local TIMES_START="$TIMES_RESULT"
-  get_times
-  local TIMES_STOP="$TIMES_RESULT"
-  local TIME1
-  local TIME2
-  local KIND
-  for KIND in 1 2
-  do
-    local START=$(echo "$TIMES_START" | cut -d " " -f $KIND)
-    local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND)
-
-    local TIME=$(( $STOP - $START ))
-    eval "TIME${KIND}=$TIME"
-
-    local SECS=$(( $TIME % 60 ))
-    [ $SECS -lt 10 ] && SECS="0$SECS"
-    local MINUTES=$(( ($TIME / 60) % 60 ))
-    [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
-    local HOURS=$(( $TIME / 3600 ))
-
-    local KIND_NAME
-    [ "$KIND" = 1 ] && KIND_NAME="elapsed time"
-    [ "$KIND" = 2 ] && KIND_NAME="cpu time"
-    local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}"
-
-    if [ ${KIND} -eq 1 -o ${TIME} -ge 5 ]; then
-      if [ -z "$TIMES_REPORT" ]; then
-        TIMES_REPORT="$RESULT"
-      else
-        TIMES_REPORT="$TIMES_REPORT, $RESULT"
-      fi
-    fi
-  done
-  if let "$TIME1 >= 5 && $TIME2 >= 5"
-  then
-    local FACTOR=$(( $TIME2 * 100 / $TIME1 ))
-    local FACTOR1=$(( $FACTOR / 100 ))
-    local FACTOR2=$(( $FACTOR % 100 ))
-    if let "$FACTOR2 < 10"; then FACTOR2="0$FACTOR2"; fi
-    TIMES_REPORT="$TIMES_REPORT, factor ${FACTOR1}.${FACTOR2}"
-  fi
-}
-
-show_times  # sets TIMES_REPORT
-
-unset TIMES_RESULT get_times show_times