[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: What is the proper way to set the default font these days?
From: |
Miles Bader |
Subject: |
Re: What is the proper way to set the default font these days? |
Date: |
Mon, 15 Jun 2009 12:29:48 +0900 |
James Cloos <address@hidden> writes:
> Miles> The "rules" (by my observation) are a bit bizarre: If there's
> Miles> _anything_ in the server's database, even entries for an
> Miles> unrelated application, then ~/.Xdefaults is completely ignored,
> Miles> and only entries from the server database are used; otherwise
> Miles> ~/.Xdefaults is used.
>
> After the above, then ~/.Xdefaults-$HOSTNAME is always read.
>
> The idea is that ~/.Xdefaults-$HOSTNAME is for settings which are
> specific to one client machine and the server's database for settings
> which are specific to one server. Reading ~/.Xdefaults is a backup
> measure for the cases where the user does not have a $HOME on the
> server.
>
> Obviously this distinction is more useful when one has multiple boxen
> with a shared /home (eg by nfs) and uses X over tcp. (That was a very
> common setup when the coding was done.)
Sure, but... now it's not.
The whole thing feels very kludgey, like they had some clever ideas
about generalizing things, but didn't spend much time trying to _debug_
those ideas to catch potential downsides and get rid of the rough edges.
[Sadly, much of the X infrastructure feels like that...]
-miles
--
"Suppose we've chosen the wrong god. Every time we go to church we're
just making him madder and madder." -- Homer Simpson
- Re: What is the proper way to set the default font these days?, (continued)
- Re: What is the proper way to set the default font these days?, Chong Yidong, 2009/06/10
- Re: What is the proper way to set the default font these days?, Chad Brown, 2009/06/08
- Re: What is the proper way to set the default font these days?, David Reitter, 2009/06/08
- Re: What is the proper way to set the default font these days?, Miles Bader, 2009/06/08
- Re: What is the proper way to set the default font these days?, Stefan Monnier, 2009/06/10
- Re: What is the proper way to set the default font these days?, Miles Bader, 2009/06/10
- Re: What is the proper way to set the default font these days?, Eli Zaretskii, 2009/06/08
- Re: What is the proper way to set the default font these days?, Johan Bockgård, 2009/06/08
- Re: What is the proper way to set the default font these days?, James Cloos, 2009/06/12
- Re: What is the proper way to set the default font these days?, Stefan Monnier, 2009/06/12
- Re: What is the proper way to set the default font these days?,
Miles Bader <=