diff options
| author | Andrei Vagin <avagin@google.com> | 2019-10-02 13:00:07 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-02 13:00:07 -0700 |
| commit | 9a875306dbabcf335a2abccc08119a1b67d0e51a (patch) | |
| tree | 0f72c12e951a5eee7156df7a5d63351bc89befa6 /tools/workspace_status.sh | |
| parent | 38bc0b6b6addd25ceec4f66ef1af41c1e61e2985 (diff) | |
| parent | 03ce4dd86c9acd6b6148f68d5d2cf025d8c254bb (diff) | |
Merge branch 'master' into pr_syscall_linux
Diffstat (limited to 'tools/workspace_status.sh')
| -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..fb09ff331 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 trigger a re-link if it changes. +echo STABLE_VERSION $(git describe --always --tags --abbrev=12 --dirty) |