# HG changeset patch
# User wenzelm
# Date 1645193263 -3600
# Node ID 7001ae6c08320832fa952419b1bc7df97af1f851
# Parent  37bd912c87657e116e878770acc04507d88c1fe0
tuned whitespace;

diff -r 37bd912c8765 -r 7001ae6c0832 src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Fri Feb 18 14:03:45 2022 +0100
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Fri Feb 18 15:07:43 2022 +0100
@@ -196,15 +196,15 @@
     table.setFillsViewportHeight(true)
     table.getTableHeader.setReorderingAllowed(false)
 
-		table.getColumnModel.getColumn(0).setPreferredWidth(30)
-		table.getColumnModel.getColumn(0).setMinWidth(30)
-		table.getColumnModel.getColumn(0).setMaxWidth(30)
-		table.getColumnModel.getColumn(0).setResizable(false)
-		table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30)
+    table.getColumnModel.getColumn(0).setPreferredWidth(30)
+    table.getColumnModel.getColumn(0).setMinWidth(30)
+    table.getColumnModel.getColumn(0).setMaxWidth(30)
+    table.getColumnModel.getColumn(0).setResizable(false)
+    table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30)
 
     val scroller = new JScrollPane(table)
-		scroller.getViewport.setBackground(table.getBackground)
-		scroller.setPreferredSize(table_size)
+    scroller.getViewport.setBackground(table.getBackground)
+    scroller.setPreferredSize(table_size)
 
     add(scroller, BorderLayout.CENTER)
   }