FreeBSD Bugzilla – Attachment 81000 Details for
Bug 116046
Update port: math/isabelle
Home
|
New
|
Browse
|
Search
|
[?]
|
Reports
|
Help
|
New Account
|
Log In
Remember
[x]
|
Forgot Password
Login:
[x]
[patch]
isabelle.diff
isabelle.diff (text/plain), 40.40 KB, created by
Timothy Bourke
on 2007-09-03 12:20:01 UTC
(
hide
)
Description:
isabelle.diff
Filename:
MIME Type:
Creator:
Timothy Bourke
Created:
2007-09-03 12:20:01 UTC
Size:
40.40 KB
patch
obsolete
>Index: Makefile >=================================================================== >RCS file: /home/ncvs/ports/math/isabelle/Makefile,v >retrieving revision 1.5 >diff -u -r1.5 Makefile >--- Makefile 19 May 2007 20:15:04 -0000 1.5 >+++ Makefile 2 Sep 2007 12:08:27 -0000 >@@ -2,12 +2,12 @@ > # Date created: 08 August 2005 > # Whom: Timothy Bourke <timbob@bigpond.com> > # >-# $FreeBSD: ports/math/isabelle/Makefile,v 1.5 2007/05/19 20:15:04 flz Exp $ >+# $FreeBSD$ > # > > PORTNAME= isabelle > PORTVERSION= 2005 >-PORTREVISION= 1 >+PORTREVISION= 2 > CATEGORIES= math > MASTER_SITES= http://isabelle.in.tum.de/dist/ \ > http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ \ >@@ -28,7 +28,7 @@ > > .if defined(WITH_SMLNJ) > ML_SYSTEM= smlnj-110 >-ML_HOME= ${LOCALBASE}/smlnj/bin >+ML_HOME= ${LOCALBASE}/bin > ML_OPTIONS= @SMLdebug=/dev/null > ML_PLATFORM= x86-bsd > .else >@@ -40,15 +40,14 @@ > .endif > > USE_PERL5= yes >-BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash > RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral > > DOCFILES= Contents *.pdf *.eps *.ps *.dvi > > .if defined(WITH_SMLNJ) > PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM} >-BUILD_DEPENDS+= sml:${PORTSDIR}/lang/sml-nj-devel >-RUN_DEPENDS+= sml:${PORTSDIR}/lang/sml-nj-devel >+BUILD_DEPENDS+= smlnj-devel>=110.65:${PORTSDIR}/lang/sml-nj-devel >+MAKE_ENV+= SMLNJ_DEVEL=yes > .else > PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM} > BUILD_DEPENDS+= poly:${PORTSDIR}/lang/polyml >@@ -77,6 +76,8 @@ > ${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings > @${RM} ${WRKSRC}/etc/settings.presed > @${TOUCH} ${WRKSRC}/contrib/.keep >+ @${REINPLACE_CMD} -e 's|%%SMLNJ_VERSION%%|SMLNJ_DEVEL=yes|' \ >+ ${WRKSRC}/lib/scripts/run-smlnj > > post-install: > ${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin >Index: pkg-plist >=================================================================== >RCS file: /home/ncvs/ports/math/isabelle/pkg-plist,v >retrieving revision 1.4 >diff -u -r1.4 pkg-plist >--- pkg-plist 22 Mar 2007 11:31:59 -0000 1.4 >+++ pkg-plist 2 Sep 2007 12:09:46 -0000 >@@ -1959,7 +1959,6 @@ > %%DATADIR%%/etc/isar-keywords.el > %%DATADIR%%/etc/proofgeneral-settings.el > %%DATADIR%%/etc/settings >-%%DATADIR%%/etc/settings.orig > %%DATADIR%%/etc/user-settings.sample > %%DATADIR%%/heaps/%%HEAPSUBDIR%%/CCL > %%DATADIR%%/heaps/%%HEAPSUBDIR%%/CTT >Index: files/Makefile >=================================================================== >RCS file: /home/ncvs/ports/math/isabelle/files/Makefile,v >retrieving revision 1.2 >diff -u -r1.2 Makefile >--- files/Makefile 1 May 2006 18:01:58 -0000 1.2 >+++ files/Makefile 2 Sep 2007 12:09:46 -0000 >@@ -19,10 +19,10 @@ > for f in ${SRCDIRS}; \ > do for g in `find -d $$f -type d`; \ > do mkdir -p ${DESTDIR}/$$g; \ >- files=`find $$g -depth 1 -type f \\! -perm +u+x`; \ >+ files=`find -E $$g -depth 1 -type f -not -regex '.*\.(bak|orig)$$' -not -perm +u+x`; \ > if [ "$$files" != "" ]; then ${BSD_INSTALL_DATA} \ > $$files ${DESTDIR}/$$g; fi; \ >- scripts=`find $$g -depth 1 -type f -perm +u+x`; \ >+ scripts=`find -E $$g -depth 1 -type f -not -regex '.*\.(bak|orig)$$' -perm +u+x`; \ > if [ "$$scripts" != "" ]; then ${BSD_INSTALL_SCRIPT} \ > $$scripts ${DESTDIR}/$$g; fi; \ > done; \ >Index: files/patch-bin-Isabelle >=================================================================== >RCS file: files/patch-bin-Isabelle >diff -N files/patch-bin-Isabelle >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-bin-Isabelle 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,8 @@ >+--- ./bin/Isabelle.orig Sun Sep 2 15:23:58 2007 >++++ ./bin/Isabelle Sun Sep 2 16:05:40 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: Isabelle,v 1.30 2005/05/17 07:58:47 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >Index: files/patch-bin-isabelle >=================================================================== >RCS file: files/patch-bin-isabelle >diff -N files/patch-bin-isabelle >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-bin-isabelle 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,8 @@ >+--- ./bin/isabelle.orig Sun Sep 2 15:23:58 2007 >++++ ./bin/isabelle Sun Sep 2 16:05:44 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: isabelle,v 1.46 2005/05/17 07:58:47 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >Index: files/patch-bin-isabelle_interface >=================================================================== >RCS file: files/patch-bin-isabelle_interface >diff -N files/patch-bin-isabelle_interface >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-bin-isabelle_interface 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,23 @@ >+--- ./bin/isabelle-interface.orig Sun Sep 2 15:23:58 2007 >++++ ./bin/isabelle-interface Sun Sep 2 16:05:48 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: isabelle-interface,v 1.8 2005/05/17 16:10:33 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -16,12 +16,12 @@ >+ PRG="$(basename "$0")" >+ >+ ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" >+-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 >++. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 >+ >+ >+ ## diagnostics >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-bin-isabelle_process >=================================================================== >RCS file: files/patch-bin-isabelle_process >diff -N files/patch-bin-isabelle_process >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-bin-isabelle_process 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,32 @@ >+--- ./bin/isabelle-process.orig Sun Sep 2 15:23:58 2007 >++++ ./bin/isabelle-process Sun Sep 2 16:05:51 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: isabelle-process,v 1.13 2005/07/19 15:21:45 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -16,12 +16,12 @@ >+ PRG="$(basename "$0")" >+ >+ ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" >+-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 >++. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 >+ >+ >+ ## diagnostics >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" >+@@ -48,7 +48,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-bin-isatool >=================================================================== >RCS file: files/patch-bin-isatool >diff -N files/patch-bin-isatool >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-bin-isatool 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,32 @@ >+--- ./bin/isatool.orig Sun Sep 2 15:23:58 2007 >++++ ./bin/isatool Sun Sep 2 16:05:57 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: isatool,v 1.22 2005/05/17 07:58:47 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -16,12 +16,12 @@ >+ PRG="$(basename "$0")" >+ >+ ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" >+-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 >++. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 >+ >+ >+ ## diagnostics >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG TOOL [ARGS ...]" >+@@ -49,7 +49,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-build >=================================================================== >RCS file: files/patch-build >diff -N files/patch-build >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-build 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,41 @@ >+--- build.orig Mon Sep 26 21:12:24 2005 >++++ build Sun Sep 2 19:02:32 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: build,v 1.35 2005/09/26 11:12:24 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -23,12 +23,12 @@ >+ PRG="$(basename "$0")" >+ >+ ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)" >+-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 >++. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 >+ >+ >+ ## diagnostics >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] [LOGICS ...]" >+@@ -46,7 +46,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ 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 >Index: files/patch-lib-Tools-browser >=================================================================== >RCS file: files/patch-lib-Tools-browser >diff -N files/patch-lib-Tools-browser >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-browser 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,26 @@ >+--- ./lib/Tools/browser.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/browser Sun Sep 2 15:47:49 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: browser,v 1.16 2004/06/21 08:25:57 kleing Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] [GRAPHFILE]" >+@@ -20,7 +20,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-lib-Tools-convert >=================================================================== >RCS file: files/patch-lib-Tools-convert >diff -N files/patch-lib-Tools-convert >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-convert 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/convert.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/convert Sun Sep 2 15:48:00 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: convert,v 1.5 2005/04/26 17:50:57 wenzelm Exp $ >+ # Author: David von Oheimb, TU Muenchen >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [FILES|DIRS...]" >Index: files/patch-lib-Tools-dimacs2hol >=================================================================== >RCS file: files/patch-lib-Tools-dimacs2hol >diff -N files/patch-lib-Tools-dimacs2hol >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-dimacs2hol 2 Sep 2007 12:09:46 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/dimacs2hol.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/dimacs2hol Sun Sep 2 15:48:05 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: dimacs2hol,v 1.3 2005/04/26 17:50:57 wenzelm Exp $ >+ # Author: Tjark Weber >+@@ -11,7 +11,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG FILES" >Index: files/patch-lib-Tools-display >=================================================================== >RCS file: files/patch-lib-Tools-display >diff -N files/patch-lib-Tools-display >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-display 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,26 @@ >+--- ./lib/Tools/display.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/display Sun Sep 2 15:48:09 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: display,v 1.8 2005/04/13 16:48:19 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] FILE" >+@@ -21,7 +21,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-lib-Tools-doc >=================================================================== >RCS file: files/patch-lib-Tools-doc >diff -N files/patch-lib-Tools-doc >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-doc 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,26 @@ >+--- ./lib/Tools/doc.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/doc Sun Sep 2 15:48:14 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: doc,v 1.13 2005/04/13 16:48:06 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [DOC]" >+@@ -18,7 +18,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-lib-Tools-document >=================================================================== >RCS file: files/patch-lib-Tools-document >diff -N files/patch-lib-Tools-document >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-document 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,44 @@ >+--- ./lib/Tools/document.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/document Sun Sep 2 15:48:20 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: document,v 1.22 2005/08/16 11:42:15 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] [DIR]" >+@@ -25,7 +25,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >+@@ -88,7 +88,7 @@ >+ >+ # tagged region markup >+ >+-function prep_tags () >++prep_tags () >+ { >+ ( >+ IFS="," >+@@ -115,7 +115,7 @@ >+ >+ # prepare document >+ >+-function pre_latex () >++pre_latex () >+ { >+ local FMT="$1" >+ [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log >Index: files/patch-lib-Tools-expandshort >=================================================================== >RCS file: files/patch-lib-Tools-expandshort >diff -N files/patch-lib-Tools-expandshort >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-expandshort 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/expandshort.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/expandshort Sun Sep 2 15:48:24 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: expandshort,v 1.15 2005/04/26 17:50:57 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [FILES|DIRS...]" >Index: files/patch-lib-Tools-findlogics >=================================================================== >RCS file: files/patch-lib-Tools-findlogics >diff -N files/patch-lib-Tools-findlogics >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-findlogics 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/findlogics.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/findlogics Sun Sep 2 15:48:27 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: findlogics,v 1.8 2004/06/21 08:25:57 kleing Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG=$(basename "$0") >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG" >Index: files/patch-lib-Tools-fixcpure >=================================================================== >RCS file: files/patch-lib-Tools-fixcpure >diff -N files/patch-lib-Tools-fixcpure >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-fixcpure 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/fixcpure.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/fixcpure Sun Sep 2 15:48:31 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: fixcpure,v 1.2 2005/04/26 17:50:57 wenzelm Exp $ >+ # Author: Makarius >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [FILES|DIRS...]" >Index: files/patch-lib-Tools-fixgreek >=================================================================== >RCS file: files/patch-lib-Tools-fixgreek >diff -N files/patch-lib-Tools-fixgreek >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-fixgreek 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/fixgreek.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/fixgreek Sun Sep 2 15:48:35 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: fixgreek,v 1.4 2005/04/26 17:50:58 wenzelm Exp $ >+ # Author: Sebastian Skalberg, TU Muenchen >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [FILES|DIRS...]" >Index: files/patch-lib-Tools-fixheaders >=================================================================== >RCS file: files/patch-lib-Tools-fixheaders >diff -N files/patch-lib-Tools-fixheaders >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-fixheaders 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/fixheaders.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/fixheaders Sun Sep 2 15:48:38 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: fixheaders,v 1.2 2005/07/06 08:34:07 wenzelm Exp $ >+ # Author: Florian Haftmann, TUM >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [FILES|DIRS...]" >Index: files/patch-lib-Tools-fixsome >=================================================================== >RCS file: files/patch-lib-Tools-fixsome >diff -N files/patch-lib-Tools-fixsome >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-fixsome 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/fixsome.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/fixsome Sun Sep 2 15:48:42 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: fixsome,v 1.7 2005/04/26 17:50:58 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [FILES|DIRS...]" >Index: files/patch-lib-Tools-getenv >=================================================================== >RCS file: files/patch-lib-Tools-getenv >diff -N files/patch-lib-Tools-getenv >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-getenv 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/getenv.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/getenv Sun Sep 2 15:48:46 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: getenv,v 1.11 2005/09/01 20:49:18 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] [VARNAMES ...]" >Index: files/patch-lib-Tools-install >=================================================================== >RCS file: files/patch-lib-Tools-install >diff -N files/patch-lib-Tools-install >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-install 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,54 @@ >+--- ./lib/Tools/install.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/install Sun Sep 2 15:52:30 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: install,v 1.25 2005/07/01 12:41:57 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG=$(basename "$0") >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS]" >+@@ -24,7 +24,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >+@@ -71,18 +71,6 @@ >+ >+ # standalone binaries >+ >+-#set by configure >+-AUTO_BASH=bash >+- >+-case "$AUTO_BASH" in >+- /*) >+- BASH="$AUTO_BASH" >+- ;; >+- *) >+- BASH="/usr/bin/env bash" >+- ;; >+-esac >+- >+ if [ -n "$BINDIR" ]; then >+ mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" >+ >+@@ -92,7 +80,7 @@ >+ DIST="$DISTDIR/bin/$NAME" >+ echo "installing $BIN" >+ rm -f "$BIN" >+- echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN" >++ echo "#!/bin/sh" > "$BIN" || fail "Cannot write file: $BIN" >+ echo >> "$BIN" >+ echo "exec \"$DIST\" \"\$@\"" >> "$BIN" >+ chmod +x "$BIN" >Index: files/patch-lib-Tools-latex >=================================================================== >RCS file: files/patch-lib-Tools-latex >diff -N files/patch-lib-Tools-latex >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-latex 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,65 @@ >+--- ./lib/Tools/latex.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/latex Sun Sep 2 15:48:54 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: latex,v 1.27 2005/07/19 15:21:45 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] [FILE]" >+@@ -23,7 +23,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >+@@ -67,7 +67,7 @@ >+ FILEBASE=$(basename "$FILE" .tex) >+ [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" >+ >+-function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } >++check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } >+ >+ >+ # operations >+@@ -75,13 +75,13 @@ >+ #set by configure >+ AUTO_PERL=perl >+ >+-function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } >+-function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } >+-function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } >+-function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } >+-function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } >+-function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } >+-function copy_styles () >++run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } >++run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } >++run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } >++run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } >++run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } >++run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } >++copy_styles () >+ { >+ for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty >+ do >+@@ -90,7 +90,7 @@ >+ done >+ } >+ >+-function extract_syms () >++extract_syms () >+ { >+ "$AUTO_PERL" -n \ >+ -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ >Index: files/patch-lib-Tools-logo >=================================================================== >RCS file: files/patch-lib-Tools-logo >diff -N files/patch-lib-Tools-logo >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-logo 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,26 @@ >+--- ./lib/Tools/logo.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/logo Sun Sep 2 15:49:00 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: logo,v 1.10 2005/04/26 17:50:58 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] NAME" >+@@ -22,7 +22,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-lib-Tools-make >=================================================================== >RCS file: files/patch-lib-Tools-make >diff -N files/patch-lib-Tools-make >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-make 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/make.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/make Sun Sep 2 15:49:08 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: make,v 1.9 2004/06/21 08:25:57 kleing Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [ARGS ...]" >Index: files/patch-lib-Tools-makeall >=================================================================== >RCS file: files/patch-lib-Tools-makeall >diff -N files/patch-lib-Tools-makeall >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-makeall 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,28 @@ >+--- lib/Tools/makeall.orig Wed Apr 27 03:50:14 2005 >++++ lib/Tools/makeall Sun Sep 2 19:04:36 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: makeall,v 1.19 2005/04/26 17:50:14 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -13,8 +13,9 @@ >+ ## diagnostics >+ >+ PRG="$(basename "$0")" >++SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` )) >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [ARGS ...]" >+@@ -24,7 +25,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-lib-Tools-mkdir >=================================================================== >RCS file: files/patch-lib-Tools-mkdir >diff -N files/patch-lib-Tools-mkdir >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-mkdir 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,26 @@ >+--- ./lib/Tools/mkdir.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/mkdir Sun Sep 2 15:49:15 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: mkdir,v 1.42 2005/06/20 20:13:55 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] [LOGIC] NAME" >+@@ -27,7 +27,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-lib-Tools-print >=================================================================== >RCS file: files/patch-lib-Tools-print >diff -N files/patch-lib-Tools-print >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-print 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,26 @@ >+--- ./lib/Tools/print.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/print Sun Sep 2 15:49:21 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: print,v 1.2 2004/06/29 09:21:18 kleing Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -8,7 +8,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] FILE" >+@@ -21,7 +21,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-lib-Tools-unsymbolize >=================================================================== >RCS file: files/patch-lib-Tools-unsymbolize >diff -N files/patch-lib-Tools-unsymbolize >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-unsymbolize 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,17 @@ >+--- ./lib/Tools/unsymbolize.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/unsymbolize Sun Sep 2 15:49:24 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: unsymbolize,v 1.6 2005/04/26 17:50:58 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [FILES|DIRS...]" >Index: files/patch-lib-Tools-usedir >=================================================================== >RCS file: files/patch-lib-Tools-usedir >diff -N files/patch-lib-Tools-usedir >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-usedir 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,57 @@ >+--- lib/Tools/usedir.orig Wed Aug 31 23:46:31 2005 >++++ lib/Tools/usedir Sun Sep 2 19:04:54 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: usedir,v 1.60 2005/08/31 13:46:31 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -10,7 +10,7 @@ >+ >+ PRG="$(basename "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS] LOGIC NAME" >+@@ -40,18 +40,18 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >+ } >+ >+-function check_bool() >++check_bool() >+ { >+ [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\"" >+ } >+ >+-function check_number() >++check_number() >+ { >+ [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" >+ } >+@@ -77,7 +77,7 @@ >+ PROOFS=0 >+ VERBOSE=false >+ >+-function getoptions() >++getoptions() >+ { >+ OPTIND=1 >+ while getopts "C:D:P:V:bc:d:f:g:i:m:p:rs:v:" OPT >+@@ -198,7 +198,7 @@ >+ fi >+ >+ >+-SECONDS=0 >++SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` )) >+ >+ if [ -n "$BUILD" ]; then >+ ITEM="$SESSION" >Index: files/patch-lib-Tools-version >=================================================================== >RCS file: files/patch-lib-Tools-version >diff -N files/patch-lib-Tools-version >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-Tools-version 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,8 @@ >+--- ./lib/Tools/version.orig Sun Sep 2 15:11:55 2007 >++++ ./lib/Tools/version Sun Sep 2 15:49:33 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: version,v 1.2 2004/06/21 08:25:57 kleing Exp $ >+ # Author: Stefan Berghofer, TU Muenchen >Index: files/patch-lib-scripts-feeder >=================================================================== >RCS file: files/patch-lib-scripts-feeder >diff -N files/patch-lib-scripts-feeder >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-feeder 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,26 @@ >+--- ./lib/scripts/feeder.orig Sun Sep 2 15:12:50 2007 >++++ ./lib/scripts/feeder Sun Sep 2 15:54:12 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: feeder,v 1.10 2005/04/26 17:50:58 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -11,7 +11,7 @@ >+ PRG="$(basename "$0")" >+ DIR="$(dirname "$0")" >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS]" >+@@ -27,7 +27,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >Index: files/patch-lib-scripts-getsettings >=================================================================== >RCS file: files/patch-lib-scripts-getsettings >diff -N files/patch-lib-scripts-getsettings >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-getsettings 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,39 @@ >+--- ./lib/scripts/getsettings.orig Sun Sep 2 15:59:52 2007 >++++ ./lib/scripts/getsettings Sun Sep 2 16:03:07 2007 >+@@ -2,7 +2,7 @@ >+ # $Id: getsettings,v 1.24 2005/06/06 07:28:28 kleing Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+ # >+-# getsettings - bash source script to augment current env. >++# getsettings - sh source script to augment current env. >+ >+ if [ -z "$ISABELLE_SETTINGS_PRESENT" ] >+ then >+@@ -24,10 +24,9 @@ >+ >+ #users tend to put strange things in here ... >+ unset ENV >+-unset BASH_ENV >+ >+ #support easy settings >+-function choosefrom () >++choosefrom () >+ { >+ local RESULT="" >+ local FILE="" >+@@ -42,13 +41,13 @@ >+ } >+ >+ #get actual settings >+-source "$ISABELLE_HOME/etc/settings" || exit 2 >++. "$ISABELLE_HOME/etc/settings" || exit 2 >+ ISABELLE_SITE_SETTINGS_PRESENT=true >+ >+ [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ >+ { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; } >+ [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \ >+- { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; } >++ { . "$ISABELLE_HOME_USER/etc/settings" || exit 2; } >+ >+ #append ML system identifier to paths >+ if [ -z "$ML_PLATFORM" ]; then >Index: files/patch-lib-scripts-patch_scripts.bash >=================================================================== >RCS file: files/patch-lib-scripts-patch_scripts.bash >diff -N files/patch-lib-scripts-patch_scripts.bash >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-patch_scripts.bash 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,37 @@ >+--- lib/scripts/patch-scripts.bash.orig Sun Sep 2 15:55:18 2007 >++++ lib/scripts/patch-scripts.bash Sun Sep 2 16:06:41 2007 >+@@ -3,12 +3,12 @@ >+ # Author: Markus Wenzel, TU Muenchen >+ # >+ # patch-scripts.bash - relocate interpreter paths of executable scripts and >+-# insert AUTO_BASH/AUTO_PERL values >++# insert AUTO_PERL values >+ # >+ >+ ## find binaries >+ >+-function findbin() >++findbin() >+ { >+ local BASE="$1" >+ local BINARY="" >+@@ -29,17 +29,14 @@ >+ >+ ## main >+ >+-[ -z "$BASH_PATH" ] && BASH_PATH=$(findbin bash) >+ [ -z "$PERL_PATH" ] && PERL_PATH=$(findbin perl) >+-[ -z "$AUTO_BASH" ] && AUTO_BASH="$BASH_PATH" >+ [ -z "$AUTO_PERL" ] && AUTO_PERL="$PERL_PATH" >+ >+ for FILE in $(find . -type f -print) >+ do >+ if [ -x "$FILE" ]; then >+- sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \ >+- -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \ >+- -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~" >++ sed -e "s:^#!.*/perl:#!$PERL_PATH:" \ >++ -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~" >+ if cmp -s "$FILE" "$FILE~~"; then >+ rm "$FILE~~" >+ else >Index: files/patch-lib-scripts-polyml_platform >=================================================================== >RCS file: files/patch-lib-scripts-polyml_platform >diff -N files/patch-lib-scripts-polyml_platform >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-polyml_platform 2 Sep 2007 12:09:52 -0000 >@@ -0,0 +1,8 @@ >+--- ./lib/scripts/polyml-platform.orig Sun Sep 2 15:13:40 2007 >++++ ./lib/scripts/polyml-platform Sun Sep 2 15:54:17 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: polyml-platform,v 1.1 2005/08/01 17:20:48 wenzelm Exp $ >+ # >Index: files/patch-lib-scripts-polyml_version >=================================================================== >RCS file: files/patch-lib-scripts-polyml_version >diff -N files/patch-lib-scripts-polyml_version >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-polyml_version 2 Sep 2007 12:09:55 -0000 >@@ -0,0 +1,8 @@ >+--- ./lib/scripts/polyml-version.orig Sun Sep 2 15:13:40 2007 >++++ ./lib/scripts/polyml-version Sun Sep 2 15:54:22 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: polyml-version,v 1.2 2005/09/15 15:18:57 wenzelm Exp $ >+ # >Index: files/patch-lib-scripts-run_mosml >=================================================================== >RCS file: files/patch-lib-scripts-run_mosml >diff -N files/patch-lib-scripts-run_mosml >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-run_mosml 2 Sep 2007 12:09:55 -0000 >@@ -0,0 +1,35 @@ >+--- lib/scripts/run-mosml.orig Mon Jun 21 18:25:58 2004 >++++ lib/scripts/run-mosml Sun Sep 2 17:14:13 2007 >+@@ -1,16 +1,14 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: run-mosml,v 1.8 2004/06/21 08:25:58 kleing Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+ # >+ # Moscow ML 2.00 startup script >+ >+-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE >+- >+ >+ ## diagnostics >+ >+-function fail_out() >++fail_out() >+ { >+ echo "Unable to create output heap file: \"$OUTFILE\"" >&2 >+ exit 2 >+@@ -37,6 +35,13 @@ >+ [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } >+ fi >+ >++SAVE_OUTFILE="$OUTFILE" >++SAVE_MLTEXT="$MLTEXT" >++SAVE_NOWRITE="$NOWRITE" >++unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE >++OUTFILE="$SAVE_OUTFILE" >++MLTEXT="$SAVE_MLTEXT" >++NOWRITE="$SAVE_NOWRITE" >+ >+ ## run it! >+ >Index: files/patch-lib-scripts-run_polyml >=================================================================== >RCS file: files/patch-lib-scripts-run_polyml >diff -N files/patch-lib-scripts-run_polyml >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-run_polyml 2 Sep 2007 12:09:55 -0000 >@@ -0,0 +1,57 @@ >+--- lib/scripts/run-polyml.orig Tue Aug 16 21:42:17 2005 >++++ lib/scripts/run-polyml Sun Sep 2 17:17:10 2007 >+@@ -1,22 +1,36 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: run-polyml,v 1.38 2005/08/16 11:42:17 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+ # >+ # Poly/ML startup script. >+ >+-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE >++SAVE_INFILE="$INFILE" >++SAVE_OUTFILE="$OUTFILE" >++SAVE_COPYDB="$COPYDB" >++SAVE_COMPRESS="$COMPRESS" >++SAVE_MLTEXT="$MLTEXT" >++SAVE_TERMINATE="$TERMINATE" >++SAVE_NOWRITE="$NOWRITE" >++unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE >++INFILE="$SAVE_INFILE" >++OUTFILE="$SAVE_OUTFILE" >++COPYDB="$SAVE_COPYDB" >++COMPRESS="$SAVE_COMPRESS" >++MLTEXT="$SAVE_MLTEXT" >++TERMINATE="$SAVE_TERMINATE" >++NOWRITE="$SAVE_NOWRITE" >+ >+ >+ ## diagnostics >+ >+-function fail_out() >++fail_out() >+ { >+ echo "Unable to create output heap file: \"$OUTFILE\"" >&2 >+ exit 2 >+ } >+ >+-function check_file() >++check_file() >+ { >+ if [ ! -f "$1" ]; then >+ echo "Unable to locate $1" >&2 >+@@ -35,11 +49,11 @@ >+ *-cygwin) >+ ML_DBASE_SUFFIX=".pmd" >+ POLY="$ML_HOME/PolyML.exe" >+- function fixpath () { cygpath -m "$@"; } >++ fixpath () { cygpath -m "$@"; } >+ ;; >+ *) >+ POLY="$ML_HOME/poly" >+- function fixpath () { echo -n "$@"; } >++ fixpath () { echo -n "$@"; } >+ ;; >+ esac >+ >Index: files/patch-lib-scripts-run_smlnj >=================================================================== >RCS file: files/patch-lib-scripts-run_smlnj >diff -N files/patch-lib-scripts-run_smlnj >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-run_smlnj 2 Sep 2007 12:09:55 -0000 >@@ -0,0 +1,68 @@ >+--- lib/scripts/run-smlnj.orig Mon Jun 21 18:25:58 2004 >++++ lib/scripts/run-smlnj Sun Sep 2 20:02:25 2007 >+@@ -5,18 +5,16 @@ >+ # >+ # SML/NJ startup script (for 110 or later). >+ >+-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE >+- >+ >+ ## diagnostics >+ >+-function fail_out() >++fail_out() >+ { >+ echo "Unable to create output heap file: \"$OUTFILE\"" >&2 >+ exit 2 >+ } >+ >+-function check_mlhome_file() >++check_mlhome_file() >+ { >+ if [ ! -f "$1" ]; then >+ echo "Unable to locate $1" >&2 >+@@ -25,7 +23,7 @@ >+ fi >+ } >+ >+-function check_heap_file() >++check_heap_file() >+ { >+ if [ ! -f "$1" ]; then >+ echo "Expected to find ML heap file $1" >&2 >+@@ -40,10 +38,8 @@ >+ ## compiler binaries >+ >+ SML="$ML_HOME/sml" >+-ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys" >+ >+ check_mlhome_file "$SML" >+-check_mlhome_file "$ARCH_N_OPSYS" >+ >+ >+ >+@@ -76,6 +72,14 @@ >+ FEEDER_OPTS="-q" >+ fi >+ >++SAVE_OUTFILE="$OUTFILE" >++SAVE_MLTEXT="$MLTEXT" >++SAVE_NOWRITE="$NOWRITE" >++unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE >++OUTFILE="$SAVE_OUTFILE" >++MLTEXT="$SAVE_MLTEXT" >++NOWRITE="$SAVE_NOWRITE" >++ >+ "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ >+ { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } >+ RC="$?" >+@@ -84,8 +88,7 @@ >+ ## fix heap file name and permissions >+ >+ if [ -n "$OUTFILE" ]; then >+- eval $("$ARCH_N_OPSYS") >+- [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS" >++ [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ML_PLATFORM" >+ HEAP="$OUTFILE.$HEAP_SUFFIX" >+ check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \ >+ [ -n "$NOWRITE" ] && chmod -w "$OUTFILE" >Index: files/patch-lib-scripts-showtime >=================================================================== >RCS file: files/patch-lib-scripts-showtime >diff -N files/patch-lib-scripts-showtime >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-lib-scripts-showtime 2 Sep 2007 12:09:55 -0000 >@@ -0,0 +1,26 @@ >+--- lib/scripts/showtime.orig Mon Jun 21 18:25:58 2004 >++++ lib/scripts/showtime Sun Sep 2 19:05:48 2007 >+@@ -1,18 +1,18 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: showtime,v 1.5 2004/06/21 08:25:58 kleing Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+ # >+ # showtime - print time. >+ >+-TIME="$1" >++TIME=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` - "$1" )) >+ >+-SECS=$[ $TIME % 60 ] >++SECS=$(( $TIME % 60 )) >+ [ $SECS -lt 10 ] && SECS="0$SECS" >+ >+-MINUTES=$[ ($TIME / 60) % 60 ] >++MINUTES=$(( ($TIME / 60) % 60 )) >+ [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES" >+ >+-HOURS=$[ $TIME / 3600 ] >++HOURS=$(( $TIME / 3600 )) >+ >+ echo "${HOURS}:${MINUTES}:${SECS}" >Index: files/patch-src-Pure-mk >=================================================================== >RCS file: files/patch-src-Pure-mk >diff -N files/patch-src-Pure-mk >--- /dev/null 1 Jan 1970 00:00:00 -0000 >+++ files/patch-src-Pure-mk 2 Sep 2007 12:09:55 -0000 >@@ -0,0 +1,35 @@ >+--- src/Pure/mk.orig Sun Jun 12 07:19:36 2005 >++++ src/Pure/mk Sun Sep 2 19:22:39 2007 >+@@ -1,4 +1,4 @@ >+-#!/usr/bin/env bash >++#!/bin/sh >+ # >+ # $Id: mk,v 1.27 2005/06/11 21:19:36 wenzelm Exp $ >+ # Author: Markus Wenzel, TU Muenchen >+@@ -10,7 +10,7 @@ >+ >+ ## diagnostics >+ >+-function usage() >++usage() >+ { >+ echo >+ echo "Usage: $PRG [OPTIONS]" >+@@ -23,7 +23,7 @@ >+ exit 1 >+ } >+ >+-function fail() >++fail() >+ { >+ echo "$1" >&2 >+ exit 2 >+@@ -81,7 +81,7 @@ >+ >+ # run isabelle >+ >+-SECONDS=0 >++SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` )) >+ >+ if [ -z "$RAW" ]; then >+ ITEM="Pure" >Index: files/run-polyml-5.0 >=================================================================== >RCS file: /home/ncvs/ports/math/isabelle/files/run-polyml-5.0,v >retrieving revision 1.1 >diff -u -r1.1 run-polyml-5.0 >--- files/run-polyml-5.0 22 Mar 2007 11:32:00 -0000 1.1 >+++ files/run-polyml-5.0 2 Sep 2007 12:09:55 -0000 >@@ -1,22 +1,20 @@ >-#!/usr/bin/env bash >+#!/bin/sh > # > # $Id: run-polyml-5.0,v 1.2 2006/12/08 21:18:35 wenzelm Exp $ > # Author: Makarius > # > # Poly/ML startup script (for 5.0) > >-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE >- > > ## diagnostics > >-function fail_out() >+fail_out() > { > echo "Unable to create output heap file: \"$OUTFILE\"" >&2 > exit 2 > } > >-function check_file() >+check_file() > { > if [ ! -f "$1" ]; then > echo "Unable to locate $1" >&2 >@@ -65,7 +63,6 @@ > rm -f "${OUTFILE}.o" || fail_out > fi > >- > ## run it! > > MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT" >@@ -77,6 +74,16 @@ > FEEDER_OPTS="-q" > fi > >+SAVE_INFILE="$INFILE" >+SAVE_OUTFILE="$OUTFILE" >+SAVE_MLTEXT="$MLTEXT" >+SAVE_NOWRITE="$NOWRITE" >+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE >+INFILE="$SAVE_INFILE" >+OUTFILE="$SAVE_OUTFILE" >+MLTEXT="$SAVE_MLTEXT" >+NOWRITE="$SAVE_NOWRITE" >+ > "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ > { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } > RC="$?"
<b>You cannot view the attachment while viewing its details because your browser does not support IFRAMEs. <a href="attachment.cgi?id=81000">View the attachment on a separate page</a>.</b>
View Attachment As Diff
View Attachment As Raw
Actions:
View
|
Diff
Attachments on
bug 116046
: 81000