Run make_dist from azure pipeline

1 files changed, 1 insertions, 1 deletions

diff --git a/make_dist b/make_dist
index 74692c4e..1b8b095e 100755
--- a/make_dist
+++ b/make_dist
@@ -85,7 +85,7 @@ if ($version_error)
     die "$whoami: version numbers are not consistent\n";
 }
 
-run("./configure --enable-doc-maintenance --enable-werror");
+run("./configure --disable-shared --enable-doc-maintenance --enable-werror");
 run("make -j8 build_manual");
 run("make distclean");
 cd("/tmp");