diff options
author | Marcus Brinkmann <marcus@gnu.org> | 2001-07-18 18:46:12 +0000 |
---|---|---|
committer | Marcus Brinkmann <marcus@gnu.org> | 2001-07-18 18:46:12 +0000 |
commit | a0faecab9371d537a3d8d18f451421bc31ef6a07 (patch) | |
tree | 4a80be474e9a9bb196265592fd447383a49057d6 /debian/servers.boot | |
parent | a9c1365872e9554de8f45cd859c57c5192b51a8e (diff) | |
download | hurd-a0faecab9371d537a3d8d18f451421bc31ef6a07.tar.gz hurd-a0faecab9371d537a3d8d18f451421bc31ef6a07.tar.bz2 hurd-a0faecab9371d537a3d8d18f451421bc31ef6a07.zip |
2001-07-18 Marcus Brinkmann <marcus@gnu.org>
* rc: Do not excempt random-seed when cleaning up /var/run. State
data should be in /var/lib (FHS) or /var/state.
* changelog: Update to current version.
* debian/servers.boot: Add die $(serverboot).
Diffstat (limited to 'debian/servers.boot')
-rw-r--r-- | debian/servers.boot | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/debian/servers.boot b/debian/servers.boot index 1ddd7b91..2eb4da05 100644 --- a/debian/servers.boot +++ b/debian/servers.boot @@ -17,3 +17,6 @@ # You can also add swap partitions to /etc/fstab. #/dev/hd0s2 $(add-linux-paging-file) +# Don't make serverboot the default pager. The real default pager will +# we started early in /libexec/rc. +die $(serverboot) |