diff options
author | Adam Retter <adam.retter@googlemail.com> | 2018-04-02 23:45:39 -0700 |
---|---|---|
committer | Facebook Github Bot <facebook-github-bot@users.noreply.github.com> | 2018-04-02 23:57:41 -0700 |
commit | 12b400e814977a82a384af62d9c02610954b0648 (patch) | |
tree | 0c181148ba1fcd72acb9d815ddd50f123236add8 /build_tools/version.sh | |
parent | 04c11b867df9190da204e38357a14d20296fb244 (diff) |
Some small improvements to the build_tools
Summary: Closes https://github.com/facebook/rocksdb/pull/3664
Differential Revision: D7459433
Pulled By: sagar0
fbshipit-source-id: 3817e5d45fc70e83cb26f9800eaa0f4566c8dc0e
Diffstat (limited to 'build_tools/version.sh')
-rwxr-xr-x | build_tools/version.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/build_tools/version.sh b/build_tools/version.sh index f3ca98cf6..4e3b9f20d 100755 --- a/build_tools/version.sh +++ b/build_tools/version.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash if [ "$#" = "0" ]; then echo "Usage: $0 major|minor|patch|full" exit 1 |