proper option for linux_arm;
authorwenzelm
Fri, 07 May 2021 13:16:50 +0200
changeset 73897 a2d3b4a90bca
parent 73895 e1432539df35
child 73898 ac6f8fff036b
proper option for linux_arm;
Admin/etc/options
--- a/Admin/etc/options	Thu May 06 23:28:30 2021 +0200
+++ b/Admin/etc/options	Fri May 07 13:16:50 2021 +0200
@@ -12,6 +12,9 @@
   -- "unpacked components for remote build services"
 
 
+option build_host_linux_arm : string = ""
+  -- "SSH user@host for remote build of heaps"
+
 option build_host_linux : string = ""
   -- "SSH user@host for remote build of heaps"