https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #7 from Jens Petersen <petersen(a)redhat.com> ---
(In reply to Fabio Valentini from comment #5)
> lean4.spec:31: E: rpm-buildroot-usage %build %cmake
-DLEAN_BUILD_TYPE="Release" -DUSE_GITHASH=OFF
-DLEAN_INSTALL_PREFIX=%{buildroot}
> lean4.spec:31: E: rpm-buildroot-usage %build %cmake
-DLEAN_BUILD_TYPE="Release" -DUSE_GITHASH=OFF
-DLEAN_INSTALL_PREFIX=%{buildroot}
Also, I'm not sure whether the `%buildroot` macro is actually defined in
%build.
I could retest but this was the only way I could get it to build: not the
prettiest I certainly agree.
https://github.com/leanprover/lean4/issues/3068 is the upstream issue I had
opened to get to this point.
--
You are receiving this mail because:
You are always notified about changes to this product and component
You are on the CC list for the bug.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
Report this comment as SPAM:
https://bugzilla.redhat.com/enter_bug.cgi?product=Bugzilla&format=rep...