Hilfe Diskussion:Syntaxhighlight

Diese Diskussionsseite dient dazu, Verbesserungen an der Hilfeseite „Syntaxhighlight“ zu besprechen. Persönliche Betrachtungen zum Thema gehören nicht hierher. Für allgemeine Wissensfragen gibt es die Auskunft.

Füge neue Diskussionsthemen unten an:

Klicke auf Abschnitt hinzufügen, um ein neues Diskussionsthema zu beginnen.

• Diskussionsregeln
• Hilfe zu Diskussionsseiten
• Sei sachlich und freundlich!
• Greife niemanden persönlich an!
• Geh von guten Absichten aus.

Zum Archiv

Wie wird ein Archiv angelegt?

Automatische Archivierung

Auf dieser Seite werden Abschnitte halbmonatlich automatisch archiviert, deren jüngster Beitrag mehr als 165 Tage zurückliegt und die mindestens einen signierten Beitrag enthalten. Um die Diskussionsseite nicht komplett zu leeren, verbleibt mindestens ein Abschnitt.

Automatische Archivierung

Auf dieser Seite werden Abschnitte montags automatisch archiviert, wenn sie mit {{Erledigt|1=--~~~~}} markiert sind und ihr jüngster signierter Beitrag mehr als 7 Tage zurückliegt. Um die Diskussionsseite nicht komplett zu leeren, verbleibt mindestens ein Abschnitt.

Pygments-Update-Rhythmus

Hallo,

ich habe mich heute mal gefragt, ob Pygments inzwischens auch Lean4 unterstützt, und nicht nur Lean3 (die sind stellenweise syntaktisch doch recht verschieden). Und siehe da: Ja, als Sprachcodes gibt es inzwischen lean, lean3 und lean4, statt nur lean. Zunächst wollte ich es einfach umseitig hinzufügen, habe mich aber entschieden, langsam zu machen. Dann habe ich erstmal ausprobiert, ob lean4 überhaupt geht und festgestellt: geht hier noch nicht. Ins Pygments-Change-Log geschaut und gesehen: ok, lean4 gibt's erst seit heute -- also eigentlich kein großes Wunder, dass es hier noch nicht geht. Aber: Weiß man, wann damit zu rechnen ist, dass die Unterstützung auch hier ankommt? Sind es eher Tage oder eher Monate? --Daniel5Ko (Diskussion) 21:36, 4. Mai 2024 (CEST)

@Daniel5Ko Heute wurde Task364249 erstellt und Patch 1027245 geschrieben. Die Chancen stehen nicht schlecht, dass die Aktualisierung in 1-3 Wochen live geht. --Raymond ^Disk. 21:47, 4. Mai 2024 (CEST)

Danke für die Info. :) --Daniel5Ko (Diskussion) 22:00, 4. Mai 2024 (CEST)

Wird wohl noch 'ne Weile dauern, angesichts der Änderungen in Task364249 von vorgestern. --Daniel5Ko (Diskussion) 23:38, 18. Mai 2024 (CEST)

Ja, da hatte ich leider nicht mit gerechnet :-( --Raymond ^Disk. 08:25, 19. Mai 2024 (CEST)