[PATCH RFT] defaultenv: boot/devboot: add a devboot boot target

[Ahmad Fatoum]

Executing devboot without arguments instructs it to use
"$global.boot.default" and thus leaves no way to use devboot as default
boot target easily.

Address this by adding a new devboot boot target that internally uses
${global.boot.devboot_default} instead of the default
${global.boot.default}.

Signed-off-by: Ahmad Fatoum <a.fatoum at barebox.org>
---
 Documentation/user/devboot.rst            | 11 +++++++++++
 defaultenv/defaultenv-2-base/boot/devboot | 10 ++++++++++
 2 files changed, 21 insertions(+)
 create mode 100755 defaultenv/defaultenv-2-base/boot/devboot

diff --git a/Documentation/user/devboot.rst b/Documentation/user/devboot.rst
index 550ab9120576..f8b2c8ec684e 100644
--- a/Documentation/user/devboot.rst
+++ b/Documentation/user/devboot.rst
@@ -200,6 +200,17 @@ script is loaded. Make them persistent with:
 ``global.hostname`` is typically derived from the device tree, but can be
 overridden.
 
+devboot boot target
+^^^^^^^^^^^^^^^^^^^
+
+Using the ``devboot`` boot target, the ``devboot`` script can be set
+as default boot target.  Example usage:
+
+.. code-block:: sh
+
+   nv boot.devboot_default=system0
+   nv boot.default=devboot
+
 Forwarding a remote build directory over the internet
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
diff --git a/defaultenv/defaultenv-2-base/boot/devboot b/defaultenv/defaultenv-2-base/boot/devboot
new file mode 100755
index 000000000000..ec75cf2f274c
--- /dev/null
+++ b/defaultenv/defaultenv-2-base/boot/devboot
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+if [ "${global.boot.devboot_default}" = "" ] ||
+   [ "${global.boot.devboot_default}" = "devboot" ] ||
+   [ "${global.boot.devboot_default}" = "/env/boot/devboot" ]; then
+    echo "Set global.boot.devboot_default to your eventual boot target!"
+    exit 1
+fi
+
+devboot "${global.boot.devboot_default}"
-- 
2.47.3