Eine aufbereitete Darstellung der Quelle

 
     
 
 
Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

Benutzer

Quelle  gutter   Sprache: unbekannt

 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/Gutter.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/Gutter.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/Gutter.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/Gutter.java 2025-04-22 22:08:05.106604316 +0200
@@ -682,7 +682,7 @@
  //{{{ Private members
 
  //{{{ Instance variables
- private static final int FOLD_MARKER_SIZE = 12;
+ public static final int FOLD_MARKER_SIZE = 12;
  private static final int SELECTION_GUTTER_WIDTH = 12;
   // The selection gutter exists only if the gutter is not expanded
 

[Dauer der Verarbeitung: 0.11 Sekunden, vorverarbeitet 2026-06-30]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Quellcodebibliothek
     Eigene Quellcodes
     Fremde Quellcodes
     Suchen

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik