blob: 5cb662ae8f235b5f5e18c2be5266d335c5774140 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
#!/bin/sh
set -e
if [ -z "$1" ]; then
make dist
else
home_rev=$(git name-rev --name-only HEAD)
make clean
git checkout "$1"
make dist
git checkout "$home_rev"
fi
|