diff options
Diffstat (limited to '.bashrc')
-rw-r--r-- | .bashrc | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -233,7 +233,10 @@ kill-remote-gpg () { ssh -O exit "$1" } -# build debs from a Linux kernel source tree *without* calling `make clean` +# build debs from a Linux kernel source tree *without* calling `make clean`. +# +# The -dbg deb takes some time to build. To get rid of it when it's +# not needed: scripts/config --disable DEBUG_INFO bindeb-pkg () { ver="$(make kernelversion)" date="$(date +%Y%m%d+%H%M)" @@ -243,7 +246,7 @@ bindeb-pkg () { KDEB_PKGVERSION=$ver-$date \ "$@" echo "sudo apt-get install \ -../{linux-image,linux-headers,linux-libc-dev}-$ver-spw_$ver-${date}_$arch.deb" +../linux-{image,headers}-$ver-spw_$ver-${date}_$arch.deb" } # --- host-specific aliases/functions |