ports/116053: Update port: math/isabelle
Timothy Bourke
timbob at bigpond.com
Mon Sep 3 13:50:01 UTC 2007
>Number: 116053
>Category: ports
>Synopsis: Update port: math/isabelle
>Confidential: no
>Severity: non-critical
>Priority: low
>Responsible: freebsd-ports-bugs
>State: open
>Quarter:
>Keywords:
>Date-Required:
>Class: maintainer-update
>Submitter-Id: current-users
>Arrival-Date: Mon Sep 03 13:50:00 GMT 2007
>Closed-Date:
>Last-Modified:
>Originator: Timothy Bourke
>Release: FreeBSD 6.1-RELEASE-p6 i386 (uname -s -r -m)
>Organization:
n/a
>Environment:
>Description:
This update ensures compatability with the latest
smlnj-devel port (committed last week).
The port now uses /bin/sh instead of bash.
Many thanks to Johannes 5 Joemann for helpful suggestions.
>How-To-Repeat:
>Fix:
--- isabelle.diff begins here ---
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 at 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="$?"
--- isabelle.diff ends here ---
>Release-Note:
>Audit-Trail:
>Unformatted:
More information about the freebsd-ports-bugs
mailing list