From 116cff40f1f5b0cc9cc0bce4e7915b0d9c429f53 Mon Sep 17 00:00:00 2001 From: flammie Date: Fri, 3 Jan 2025 12:12:26 +0000 Subject: [PATCH] deploy: ebf98a8ad1b67153d2b1c95290257dc802a9a616 --- Makefile.in | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile.in b/Makefile.in index 6f8d9efa4..1980dc2e0 100644 --- a/Makefile.in +++ b/Makefile.in @@ -383,6 +383,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@