Processed: Re: grub-efi: bashism in /bin/sh script

[Debian Bug Tracking System]

Processing commands for control at bugs.debian.org:

> user debian-release at lists.debian.org
Setting user to debian-release at lists.debian.org (was vincent at zweije.nl.eu.org).
> usertag 486039 -goal-dash
Bug#486039: grub-efi: bashism in /bin/sh script
Usertags were: goal-dash.
Usertags are now: .
> tag 486039 patch
Bug#486039: grub-efi: bashism in /bin/sh script
There were no tags set.
Tags added: patch

> severity 486039 minor
Bug#486039: grub-efi: bashism in /bin/sh script
Severity set to `minor' from `important'

> usertag 486043 -goal-dash
Bug#486043: grub-efi: bashism in /bin/sh script
There were no usertags set.
Usertags are now: .
> tag 486043 patch
Bug#486043: grub-efi: bashism in /bin/sh script
There were no tags set.
Tags added: patch

> severity 486043 minor
Bug#486043: grub-efi: bashism in /bin/sh script
Severity set to `minor' from `important'

> thanks
Stopping processing here.

Please contact me if you need assistance.

Debian bug tracking system administrator
(administrator, Debian Bugs database)