diff options
| -rw-r--r-- | lang/sml-nj-devel/files/patch-ab | 15 | ||||
| -rw-r--r-- | lang/sml-nj/files/patch-ab | 15 |
2 files changed, 30 insertions, 0 deletions
diff --git a/lang/sml-nj-devel/files/patch-ab b/lang/sml-nj-devel/files/patch-ab new file mode 100644 index 0000000..b54e8f0 --- /dev/null +++ b/lang/sml-nj-devel/files/patch-ab @@ -0,0 +1,15 @@ +--- config/install.sh-- Wed Aug 5 13:43:43 1998 ++++ config/install.sh Mon Feb 1 15:57:31 1999 +@@ -193,6 +193,12 @@ + exit 1 + fi + fi ++# we need to patch just before build ++patch_file="${FILESDIR}/patch-global-names" ++if [ -f $patch_file ]; then ++ echo "applying source patches" ++ $PATCH $PATCH_ARGS < $patch_file ++fi + cd $SRCDIR + + # diff --git a/lang/sml-nj/files/patch-ab b/lang/sml-nj/files/patch-ab new file mode 100644 index 0000000..b54e8f0 --- /dev/null +++ b/lang/sml-nj/files/patch-ab @@ -0,0 +1,15 @@ +--- config/install.sh-- Wed Aug 5 13:43:43 1998 ++++ config/install.sh Mon Feb 1 15:57:31 1999 +@@ -193,6 +193,12 @@ + exit 1 + fi + fi ++# we need to patch just before build ++patch_file="${FILESDIR}/patch-global-names" ++if [ -f $patch_file ]; then ++ echo "applying source patches" ++ $PATCH $PATCH_ARGS < $patch_file ++fi + cd $SRCDIR + + # |
