diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/workspace_status.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/workspace_status.sh b/tools/workspace_status.sh index 64a905fc9..6d961625e 100755 --- a/tools/workspace_status.sh +++ b/tools/workspace_status.sh @@ -14,4 +14,5 @@ # See the License for the specific language governing permissions and # limitations under the License. -echo VERSION $(git describe --always --tags --abbrev=12 --dirty) +# The STABLE_ prefix will triger a re-link if it changes. +echo STABLE_VERSION $(git describe --always --tags --abbrev=12 --dirty) |