# HG changeset patch
# User wenzelm
# Date 1597314824 -7200
# Node ID 6e8b5cdd4ba0a13f62537d7ffc004b0b1f8de534
# Parent  262d3c11a24da61a766a9dfc7868e7e3cb0baff2
tuned;

diff -r 262d3c11a24d -r 6e8b5cdd4ba0 src/Tools/jEdit/src/ml_status.scala
--- a/src/Tools/jEdit/src/ml_status.scala	Thu Aug 13 12:29:39 2020 +0200
+++ b/src/Tools/jEdit/src/ml_status.scala	Thu Aug 13 12:33:44 2020 +0200
@@ -78,7 +78,7 @@
               status.heap_used_fraction)
         }
 
-      val width_fraction = (width * fraction).toInt
+      val width2 = (width * fraction).toInt
 
       val text_bounds = gfx.getFont.getStringBounds(text, font_render_context)
       val text_x = insets.left + ((width - text_bounds.getWidth).toInt / 2)
@@ -90,15 +90,14 @@
           RenderingHints.VALUE_TEXT_ANTIALIAS_ON)
 
       gfx.setColor(progress_background)
-      gfx.fillRect(insets.left, insets.top, width_fraction, height)
+      gfx.fillRect(insets.left, insets.top, width2, height)
 
       gfx.setColor(progress_foreground)
-      gfx.setClip(insets.left, insets.top, width_fraction, height)
+      gfx.setClip(insets.left, insets.top, width2, height)
       gfx.drawString(text, text_x, text_y)
 
       gfx.setColor(getForeground)
-      gfx.setClip(insets.left + width_fraction, insets.top,
-        getWidth - insets.left - width_fraction, height)
+      gfx.setClip(insets.left + width2, insets.top, getWidth - insets.left - width2, height)
       gfx.drawString(text, text_x, text_y)
     }