mirror of
https://github.com/gentoo-mirror/gentoo.git
synced 2026-08-21 17:58:07 -07:00
Signed-off-by: Yuan Liao <liaoyuan@gmail.com>
Closes: 282a51b4d0
Signed-off-by: Miroslav Šulc <fordfrog@gentoo.org>
32 lines
880 B
Diff
32 lines
880 B
Diff
From b8d50d44ba1c0e4b5bf297f7499ad0fb5b82706e Mon Sep 17 00:00:00 2001
|
|
From: Yuan Liao <liaoyuan@gmail.com>
|
|
Date: Wed, 19 Jan 2022 10:09:14 -0800
|
|
Subject: [PATCH] build.xml: Add target that prints JVM system properties os.*
|
|
|
|
The Gentoo custom JNI Makefile needs some of those properties.
|
|
|
|
Signed-off-by: Yuan Liao <liaoyuan@gmail.com>
|
|
---
|
|
build.xml | 5 +++++
|
|
1 file changed, 5 insertions(+)
|
|
|
|
diff --git a/build.xml b/build.xml
|
|
index b7940ab..96e52ea 100644
|
|
--- a/build.xml
|
|
+++ b/build.xml
|
|
@@ -62,6 +62,11 @@
|
|
<javaversion atleast="10"/>
|
|
</condition>
|
|
|
|
+ <target name="os-props"
|
|
+ description="echo values of JVM system properties os.* to file os.properties">
|
|
+ <echoproperties prefix="os." destfile="os.properties" />
|
|
+ </target>
|
|
+
|
|
<target name="clean" description="clean working copy">
|
|
<delete dir="${build}" />
|
|
<delete dir="${dist}" />
|
|
--
|
|
2.34.1
|
|
|