src/Pure/General/path.scala
changeset 76017 9ca22009c2d0
parent 75926 b8ee1ef948c2
child 76348 a15f16e8ad18
--- a/src/Pure/General/path.scala	Mon Aug 29 16:49:42 2022 +0200
+++ b/src/Pure/General/path.scala	Mon Aug 29 19:14:04 2022 +0200
@@ -252,7 +252,8 @@
   }
 
   def exe: Path = ext("exe")
-  def platform_exe: Path = if (Platform.is_windows) exe else this
+  def exe_if(b: Boolean): Path = if (b) exe else this
+  def platform_exe: Path = exe_if(Platform.is_windows)
 
   private val Ext = new Regex("(.*)\\.([^.]*)")