1 files changed, 0 insertions, 26 deletions
diff --git a/math/isabelle/files/patch-lib-scripts-feeder b/math/isabelle/files/patch-lib-scripts-feeder
deleted file mode 100644
index 2c0963651e3a..000000000000
--- a/math/isabelle/files/patch-lib-scripts-feeder
+++ /dev/null
@@ -1,26 +0,0 @@
---- ./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