diff options
Diffstat (limited to 'math/isabelle/files/patch-lib-Tools-logo')
| -rw-r--r-- | math/isabelle/files/patch-lib-Tools-logo | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/math/isabelle/files/patch-lib-Tools-logo b/math/isabelle/files/patch-lib-Tools-logo deleted file mode 100644 index 96d4abb02507..000000000000 --- a/math/isabelle/files/patch-lib-Tools-logo +++ /dev/null @@ -1,26 +0,0 @@ ---- ./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 |
