diff --git a/collects/string-constants/private/german-string-constants.rkt b/collects/string-constants/private/german-string-constants.rkt index 96688044cd..dad6c11e0a 100644 --- a/collects/string-constants/private/german-string-constants.rkt +++ b/collects/string-constants/private/german-string-constants.rkt @@ -198,7 +198,7 @@ (error-erasing-log-directory "Fehler beim Löschen des Protokoll-Verzeichnisses.\n\n~a\n") ;; menu items connected to the logger -- also in a button in the planet status line in the drs frame - (show-log "&Log anzeigen") + (show-log "&Log einblenden") (hide-log "&Log ausblenden") (logging-all "Alle") ;; in the logging window in drscheme, shows all logs simultaneously @@ -1561,4 +1561,10 @@ (show-optimization-coach "Optimierungs-Coach einblenden") + ;; labels used (in a big font) in the background of the definitions and interactions windows + (definitions-window-label "Definitionen") + (interactions-window-label "Interaktionen") + (hide-defs/ints-label "Definitionen/Interaktionen-Beschriftung ausblenden") ;; popup menu + (show-defs/ints-label "Definitionen/Interaktionen-Beschriftung einblenden") ;; preferences checkbox + )