Skip to content

Makefile.in: fix handling of $DESTDIR #1190

Makefile.in: fix handling of $DESTDIR

Makefile.in: fix handling of $DESTDIR #1190

Triggered via push January 23, 2024 10:40
Status Success
Total duration 30m 14s
Artifacts
This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

CI.yml

on: push
Ubuntu GCC, Code Coverage (x10)
30m 5s
Ubuntu GCC, Code Coverage (x10)
Ubuntu GCC with NTL (assert, x2)
7m 14s
Ubuntu GCC with NTL (assert, x2)
macOS GCC with BLAS (x3)
16m 30s
macOS GCC with BLAS (x3)
FreeBSD Clang (x0.5)
17m 4s
FreeBSD Clang (x0.5)
Cygwin GCC (x0.5)
20m 56s
Cygwin GCC (x0.5)
Ubuntu Clang with examples (x5)
12m 37s
Ubuntu Clang with examples (x5)
Ubuntu GCC, CMake (1x)
6m 30s
Ubuntu GCC, CMake (1x)
MinGW GCC (x0.5)
10m 32s
MinGW GCC (x0.5)
MSVC (x1)
11m 24s
MSVC (x1)
Alpine Linux, musl, 32-bit (assert, x1.5)
13m 13s
Alpine Linux, musl, 32-bit (assert, x1.5)
Nemo.jl (temporary branch)
9m 58s
Nemo.jl (temporary branch)
Fit to window
Zoom out
Zoom in