diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure b/configure index 403982c69fb..f26e2ba5cb7 100755 --- a/configure +++ b/configure @@ -4809,7 +4809,7 @@ fi # Check for PPL ppl_major_version=0 ppl_minor_version=10 -ppllibs= +ppllibs=" -lppl_c -lppl -lgmpxx " pplinc= |