From d1180e98db3f1b972fe6fbffe3f06ed53ab5846c Mon Sep 17 00:00:00 2001 From: flammie Date: Fri, 3 Jan 2025 12:11:32 +0000 Subject: [PATCH] deploy: 1adde88e629c2aebc5b31f7917cce0fb039ad5b1 --- Makefile.in | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile.in b/Makefile.in index 59dfcc12..c7fd7ba4 100644 --- a/Makefile.in +++ b/Makefile.in @@ -384,6 +384,7 @@ docdir = @docdir@ dvidir = @dvidir@ exec_prefix = @exec_prefix@ gt_SHARED_common = @gt_SHARED_common@ +gt_SHARED_mul = @gt_SHARED_mul@ gt_SHARED_smi = @gt_SHARED_smi@ host = @host@ host_alias = @host_alias@