diff options
| author | Ludovic Courtès <ludo@gnu.org> | 2017-09-21 22:30:59 +0200 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2017-09-21 22:30:59 +0200 |
| commit | db4e8fd5d4a07d3be8ce68fb96722ef7077c0eee (patch) | |
| tree | 6376f7c744e71b089bdea3bc78d7e151acdc034d /gnu/system | |
| parent | e2a95f8b16674ae2965bf155b6d28ca5942abb03 (diff) | |
| download | patches-db4e8fd5d4a07d3be8ce68fb96722ef7077c0eee.tar patches-db4e8fd5d4a07d3be8ce68fb96722ef7077c0eee.tar.gz | |
system: <boot-parameters> does not use "/dev" device names.
Fixes <https://bugs.gnu.org/28445>.
Reported by Mark H Weaver and Roel Janssen.
* gnu/system.scm (read-boot-parameters)[ensure-not-/dev]: New procedure.
Use it.
Diffstat (limited to 'gnu/system')
0 files changed, 0 insertions, 0 deletions