diff options
Diffstat (limited to 'dev-ml/zarith/files/zarith-1.0-optnotrequired.patch')
| -rw-r--r-- | dev-ml/zarith/files/zarith-1.0-optnotrequired.patch | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/dev-ml/zarith/files/zarith-1.0-optnotrequired.patch b/dev-ml/zarith/files/zarith-1.0-optnotrequired.patch new file mode 100644 index 000000000..2bd1b4df8 --- /dev/null +++ b/dev-ml/zarith/files/zarith-1.0-optnotrequired.patch @@ -0,0 +1,22 @@ +From: Mehdi Dogguy <mehdi@debian.org> +Date: Sun, 2 Oct 2011 11:53:22 +0200 +Subject: [PATCH] ocamlopt is not really required + +--- + configure | 2 +- + 1 files changed, 1 insertions(+), 1 deletions(-) + +diff --git a/configure b/configure +index 5bd80d3..980aedd 100755 +--- a/configure ++++ b/configure +@@ -186,7 +186,7 @@ checkcc() + + searchbinreq $ocaml + searchbinreq $ocamlc +-searchbinreq $ocamlopt ++searchbin $ocamlopt + searchbinreq $ocamldep + searchbinreq $ocamlmklib + searchbinreq $ocamldoc +-- |