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("(.*)\\.([^.]*)")