# HG changeset patch
# User wenzelm
# Date 1672072616 -3600
# Node ID 563939d757703e6f8b02995d641fc25f43eb9ae8
# Parent  caeb732db09f8f46f48c6157ead0d021f27a96d0
tuned signature: avoid name confusion;

diff -r caeb732db09f -r 563939d75770 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Dec 26 16:57:07 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Dec 26 17:36:56 2022 +0100
@@ -116,7 +116,7 @@
     def content(): Bytes = Bytes(this.buf, 0, this.count)
   }
 
-  private class File_Content(buffer: Buffer)
+  private class File_Content_Request(buffer: Buffer)
   extends BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath) {
     def _run(): Unit = {}
     def content(): Bytes = {
@@ -126,7 +126,7 @@
     }
   }
 
-  def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
+  def make_file_content(buffer: Buffer): Bytes = (new File_Content_Request(buffer)).content()
 
 
   /* theory text edits */