Code

Further fixes to $DESTDIR handling#1611

Code

Merged

albinahlback merged 1 commit intoflintlib:flint-3.0flintlib/flint:flint-3.0from mezzarobba:destdirmezzarobba/flint:destdirCopy head branch name to clipboardJan 23, 2024

+27-27

Commits

Commits on Nov 13, 2023

• Makefile.in: fix handling of $DESTDIR

  Show description for 57c5e32
  mezzarobba

  committed
  57c5e32

  Copy full SHA for 57c5e32