From 946c12e9ee8ec58e574cbaf623a009112435b5ff Mon Sep 17 00:00:00 2001 From: =?utf8?q?Vladim=C3=ADr=20Vondru=C5=A1?= Date: Tue, 21 Feb 2023 11:48:47 +0100 Subject: [PATCH] doc: update command line for Pygments CSS generation. --- doc/css/themes.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/css/themes.rst b/doc/css/themes.rst index 85480c68..77bbe8fb 100644 --- a/doc/css/themes.rst +++ b/doc/css/themes.rst @@ -137,10 +137,10 @@ then generate a CSS file out of it: .. code:: sh - sudo cp pygments-dark.py /usr/lib/python3.8/site-packages/pygments/styles/dark.py + sudo cp pygments-dark.py /usr/lib/python3.10/site-packages/pygments/styles/dark.py pygmentize -f html -S dark -a .m-code > pygments-dark.css - sudo cp pygments-console.py /usr/lib/python3.8/site-packages/pygments/styles/console.py + sudo cp pygments-console.py /usr/lib/python3.10/site-packages/pygments/styles/console.py pygmentize -f html -S console -a .m-console > pygments-console.css Alternatively, you can use any of the builtin styles --- pick the one you like -- 2.30.2