summaryrefslogtreecommitdiff
path: root/math/isabelle/files/patch-lib-Tools-logo
diff options
context:
space:
mode:
Diffstat (limited to 'math/isabelle/files/patch-lib-Tools-logo')
-rw-r--r--math/isabelle/files/patch-lib-Tools-logo26
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