diff options
| author | Kito Cheng <kito.cheng@sifive.com> | 2020-11-05 10:46:20 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-05 10:46:20 +0800 |
| commit | 8b7811aafcbd06a202c659cf9a3937746f715b18 (patch) | |
| tree | 3b04264d8759a5738169d89b0b0a2b2a3f672719 | |
| parent | ed53ae7a71dfc6df1940c2255aea5bf542a9c422 (diff) | |
| parent | 620887bea83ed9016c7552f72ac72e908b2c105a (diff) | |
| download | riscv-gnu-toolchain-8b7811aafcbd06a202c659cf9a3937746f715b18.zip riscv-gnu-toolchain-8b7811aafcbd06a202c659cf9a3937746f715b18.tar.gz riscv-gnu-toolchain-8b7811aafcbd06a202c659cf9a3937746f715b18.tar.bz2 | |
Merge pull request #763 from AntonKrug/master
Vagrant plugin check so it will not fail in the middle of provisioning
| -rw-r--r-- | contrib/Vagrantfile | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/contrib/Vagrantfile b/contrib/Vagrantfile index c5e18d1..198d90b 100644 --- a/contrib/Vagrantfile +++ b/contrib/Vagrantfile @@ -1,3 +1,8 @@ +# Check if required plugin is installed +unless Vagrant.has_plugin?("vagrant-disksize") + raise 'The vagrant-disksize plugin is not installed! Type "vagrant plugin install vagrant-disksize" to install it.' +end + Vagrant.configure("2") do |config| config.vm.box = "ubuntu/bionic64" # needs vagrant plugin install vagrant-disksize: |