Build script for 20.04 (#1004)
Should be able to build 16.04, 18.04 and 20.04, as well as branch builds.
This commit is contained in:
@@ -15,13 +15,7 @@ sudo sed -i -e 's/splash//' /etc/default/grub
|
||||
sudo sed -i -e 's/quiet/text/' /etc/default/grub
|
||||
sudo update-grub
|
||||
# Update from official archive
|
||||
sudo apt-get update
|
||||
# 12.10 and earlier
|
||||
#sudo sed -i -e 's/us.archive.ubuntu.com/mirrors.kernel.org/' \
|
||||
# /etc/apt/sources.list
|
||||
# 13.04 and later
|
||||
#sudo sed -i -e 's/\/archive.ubuntu.com/\/mirrors.kernel.org/' \
|
||||
# /etc/apt/sources.list
|
||||
sudo apt-get -qq update
|
||||
# Clean up vmware easy install junk if present
|
||||
if [ -e /etc/issue.backup ]; then
|
||||
sudo mv /etc/issue.backup /etc/issue
|
||||
@@ -34,11 +28,10 @@ sudo apt-get -y install git-core openssh-server
|
||||
git clone git://github.com/mininet/mininet
|
||||
# Optionally check out branch
|
||||
if [ "$1" != "" ]; then
|
||||
pushd mininet
|
||||
#git checkout -b $1 $1
|
||||
# TODO branch will in detached HEAD state if it is not master
|
||||
git checkout $1
|
||||
popd
|
||||
pushd mininet
|
||||
git fetch origin $1
|
||||
git checkout $1
|
||||
popd
|
||||
fi
|
||||
# Install Mininet
|
||||
time mininet/util/install.sh
|
||||
|
||||
Reference in New Issue
Block a user