On Saturday, April 30, 2022 at 10:59:59 PM UTC-7 hohoa...@gmail.com wrote: > $SAGE_ROOT/src/bin: > > - sage.src.bin.resolvelinks.dot (factored out from > *'sage-env')* > - sage.src.bin.sage-env.dot (factored out from > *'sage-env')* > - sage.src.bin.sage-env.mod (sources > *'sage.src.bin.resolvelinks.dot'* and *'sage.src.bin.sage-env.dot')* > - *sage.src.bin.sage.dot (factored out from original > 'sage'*) > - sage.src.bin.sage.mod (sources > *'sage.src.bin.resolvelinks.dot*' and* 'sage.src.bin.sage.dot')* > - sage.src.bin.sage-sage-env-common.dot (common between > * 'sage.src.bin.sage-env.mod'* and *'sage.src.bin.sage.mod'* > > Overall, I'm skeptical that adding all of these files is a good idea. These files would have to be installed -- and would therefore clutter not only this source directory but also the installation directory. I think the people who maintain distribution packages would not be happy about this.
-- 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/c7da9b7f-090d-43a8-8993-574170815645n%40googlegroups.com.