Use LINUX_VERSION in update_linux, if defined

Author: johnousterhout

cloudlab/bin/update_linux

@@ -1,6 +1,6 @@
 #!/bin/bash
 
-# Copyright (c) 2020-2023 Homa Developers
+# Copyright (c) 2020-2026 Homa Developers
 # SPDX-License-Identifier: BSD-1-Clause
 
 # This script uses files on the current machine to update the kernel one
@@ -15,8 +15,8 @@
 # (e.g. "update_linux 4 2" means node2 through node5 will be updated).
 # "first" defaults to 1.
 
-v=`uname -r`
-#v=5.17.7+
+v="${LINUX_VERSION:-$(uname -r)}"
+echo Using version $v
 
 if [ $# -eq 2 ]; then
     first=$2