diff options
Diffstat (limited to 'dev-ml/findlib/files')
| -rw-r--r-- | dev-ml/findlib/files/findlib-1.9.7-gentoo.patch | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/dev-ml/findlib/files/findlib-1.9.7-gentoo.patch b/dev-ml/findlib/files/findlib-1.9.7-gentoo.patch deleted file mode 100644 index 2267e4289b42..000000000000 --- a/dev-ml/findlib/files/findlib-1.9.7-gentoo.patch +++ /dev/null @@ -1,13 +0,0 @@ ---- a/configure 2024-11-17 15:38:27.712271339 +0100 -+++ b/configure 2024-11-17 15:40:42.865323210 +0100 -@@ -562,6 +562,10 @@ - exit 1 - fi - -+dynlink_subdir="+dynlink" -+dynlink_dir="dynlink" -+unix_dir="unix" -+str_dir="str" - check_library dynlink '' dynlink/dynlink.cmi dynlink.cmi - check_library bigarray 'possible since 4.08' - check_library compiler-libs '' 'compiler-libs' |