Diese Seite erklärt unseren hauseigenen Linter.
Was ist ein Linter?
Der Linter ist ein Werkzeug für Autorinnen und Autoren, welches ihnen im Editor Hinweise für richtige Formatierungen gibt. Er zeigt Hinweise und Warnungen an, wenn Texte anders formatiert sind, als wir es unterstützen. Auch gibt es Hilfestellungen für richtige Formatierungen:
Bildschirmfoto des Linters
Deaktivierung des Linters
Der Linter ist standardmäßig aktiviert. Diesen kannst du über die Einstellungen auch wieder deaktivieren:
Schritt 1: Klick auf „Einstellungen“
Schritt 2: Klick auf „Helferlein“
Schritt 3: Option „Linter für Mathe für Nicht-Freaks“ deaktivieren und speichern. Hier kannst du hinterher den Linter auch wieder aktivieren.
This article is issued from Wikibooks. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.