From 0106ca3becc3bca72ee4dab9ea3198989b1ed7f5 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 3 Jul 2025 17:50:21 +0100 Subject: [PATCH] fix: undefined symbol without `LEAN_USE_GMP` (#9106) This PR fixes `undefined symbol: lean::mpz::divexact(lean::mpz const&, lean::mpz const&)` when building without `LEAN_USE_GMP` This fixes a regression in #8089 --- src/runtime/mpz.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/runtime/mpz.cpp b/src/runtime/mpz.cpp index e402f2aa20..174b12c112 100644 --- a/src/runtime/mpz.cpp +++ b/src/runtime/mpz.cpp @@ -763,7 +763,7 @@ mpz & mpz::operator%=(mpz const & o) { return rem(o.m_size, o.m_digits); } -mpz divexact(mpz const & n, mpz const & d) { +mpz mpz::divexact(mpz const & n, mpz const & d) { return n / d; }