remove "StatisticsSummary" related stuff
7 views
Skip to first unread message
Qian Yun
Oct 29, 2023, 7:08:23 AM10/29/23
to fricas-devel
I suggest to remove "StatisticsSummary" related stuff, because
they are basically empty right now, and there's no clue what
they were supposed to do.
Including:
statisticsSummary
$printStatisticsSummaryIfTrue and ')set message summary' option
statisticsInitialization
- Qian
they are basically empty right now, and there's no clue what
they were supposed to do.
Including:
statisticsSummary
$printStatisticsSummaryIfTrue and ')set message summary' option
statisticsInitialization
- Qian
Waldek Hebisch
Oct 29, 2023, 7:32:55 AM10/29/23
to fricas...@googlegroups.com
--
Waldek Hebisch
Reply all
Reply to author
Forward
0 new messages