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@