diff --git a/configure.in b/configure.in index 5c23196afd1..19f8ba7ff02 100644 --- a/configure.in +++ b/configure.in @@ -1288,6 +1288,12 @@ cat<