Hi, On Tue, May 26, 2020 at 08:46:42AM -0700, Matthias Koeppe wrote: > In general, to add a configure option, you can always do the following: > > ./configure $(./config.status --config) --enable-bar
Nice tip, tanks ! Thierry > > Matthias > > > -- > You received this message because you are subscribed to the Google Groups > "sage-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sage-devel+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sage-devel/d0d81021-58da-45ec-a2e7-cf5cc69f58a8%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/20200526155842.ebkwa5a7kmzg4brw%40metelu.net.