diff options
author | Satoshi Asami <asami@FreeBSD.org> | 2000-10-07 22:28:28 +0000 |
---|---|---|
committer | Satoshi Asami <asami@FreeBSD.org> | 2000-10-07 22:28:28 +0000 |
commit | 45088c8848de5866ad108c482399a9300fd673aa (patch) | |
tree | 697a69b255f5ed258c750b76bc82116b296613eb /lang/sml-nj | |
parent | Rename ${FILESDIR}/patch-* to ${PATCHDIR}/extra-patch-*. (diff) |
Rename ${FILISDER}/patch-* to ${FILESDIRA}/extra-patch-*. (These patches
are applied from within the configure script, patched by patch-ab.)
Diffstat (limited to 'lang/sml-nj')
-rw-r--r-- | lang/sml-nj/files/patch-ab | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lang/sml-nj/files/patch-ab b/lang/sml-nj/files/patch-ab index d8af8af38993..6e9c75bb0469 100644 --- a/lang/sml-nj/files/patch-ab +++ b/lang/sml-nj/files/patch-ab @@ -6,12 +6,12 @@ fi +# we need to patch just before build +echo "applying source patches" -+patch_file="${FILESDIR}/patch-global-names" ++patch_file="${FILESDIR}/extra-patch-global-names" +if [ -f $patch_file ]; then + $PATCH $PATCH_ARGS < $patch_file +fi +if grep -w FPE_INTDIV /usr/include/machine/trap.h > /dev/null 2>&1; then -+ patch_file="${FILESDIR}/patch-signals" ++ patch_file="${FILESDIR}/extra-patch-signals" + if [ -f $patch_file ]; then + $PATCH $PATCH_ARGS < $patch_file + fi |