diff options
author | gVisor bot <gvisor-bot@google.com> | 2019-09-12 14:55:24 -0700 |
---|---|---|
committer | gVisor bot <gvisor-bot@google.com> | 2019-09-12 14:55:24 -0700 |
commit | 78cfbbda4bcf29cc445f2ac000d4f2f9c72123f6 (patch) | |
tree | 744e315a718e47a6e29124ba992869d68a6b9e8b /tools | |
parent | 857940d30d3a8dbb099bad43954fe8062b70461d (diff) | |
parent | c1a8275b470fe0d8390cba166d4937059fd89b8b (diff) |
Merge pull request #843 from nlacasse:version
PiperOrigin-RevId: 268772451
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..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) |