Sun, 26 Jul 2020 21:53:29 +0200 proper pretty printing for latex output, notably for pide_session=true (default);
wenzelm [Sun, 26 Jul 2020 21:53:29 +0200] rev 72075
proper pretty printing for latex output, notably for pide_session=true (default);
Sat, 25 Jul 2020 23:23:59 +0200 clarified name to avoid duplication (no distinction of data on host = lrzcloud2);
wenzelm [Sat, 25 Jul 2020 23:23:59 +0200] rev 72074
clarified name to avoid duplication (no distinction of data on host = lrzcloud2);
Sat, 25 Jul 2020 21:09:46 +0200 clarified names;
wenzelm [Sat, 25 Jul 2020 21:09:46 +0200] rev 72073
clarified names;
Sat, 25 Jul 2020 12:43:29 +0200 more errors;
wenzelm [Sat, 25 Jul 2020 12:43:29 +0200] rev 72072
more errors;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 tip