diff options
Diffstat (limited to 'math/isabelle/files/patch-build')
| -rw-r--r-- | math/isabelle/files/patch-build | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/math/isabelle/files/patch-build b/math/isabelle/files/patch-build index c95bf5db4b84..0d1a9733276c 100644 --- a/math/isabelle/files/patch-build +++ b/math/isabelle/files/patch-build @@ -1,10 +1,10 @@ ---- build.orig Mon Sep 26 21:12:24 2005 -+++ build Sun Sep 2 19:02:32 2007 +--- build.orig Sat Jan 12 16:44:25 2008 ++++ build Sat Jan 12 16:46:08 2008 @@ -1,4 +1,4 @@ -#!/usr/bin/env bash +#!/bin/sh # - # $Id: build,v 1.35 2005/09/26 11:12:24 wenzelm Exp $ + # $Id: build,v 1.36 2005/12/01 17:41:46 wenzelm Exp $ # Author: Markus Wenzel, TU Muenchen @@ -23,12 +23,12 @@ PRG="$(basename "$0")" @@ -30,12 +30,3 @@ { echo "$1" >&2 exit 2 -@@ -169,7 +169,7 @@ - - # build it - --SECONDS=0 -+SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` )) - echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" - - for L in $MAKE_LOGICS |