Greetings.
On 30 Mar 2018, at 15:44, David Storrs wrote:
On Thu, Mar 29, 2018 at 5:54 PM, HiPhish <hiph...@openmailbox.org>
wrote:
I think you are trying to solve the wrong problem. If people want to
use a
command-line tool they should know how to use the command line first.
They
[...]
I look at it the other way: there are clear benefits to NOT having
names containing characters that need to be quoted, so any use of such
characters has an opportunity cost. What benefit does the space
provide that outweighs that opportunity cost?
I think the main benefit is simply that it looks nice.
OSX ^W macOS is primarily [1] designed for GUI users. The Finder has no
problem with files containing spaces, or other bash-annoying characters
such as various brackets, dollar-signs and ampersands. I can name a
file 'A&B $/€/£ conversions (2017)' and not think twice about it.
Spaces in the Racket installation locations represent a mild
inconvenience only to the minority of users (including me) who use the
command line more than the Finder, and we, to a first approximation,
don't count.
If I find such a name inconvenient, then I can either find the tab key
on my keyboard, or add a symlink somewhere convenient (as suggested
above, and what I actually do), or else learn to love the bit of the
bash manual about quoting arguments (which one should do anyway, when
writing half-way-careful scripts).
Catering to command-line users in this way, and naming
A-and-B_USD-EUR-GPB_conversions-2017 is frankly ugly, significantly less
readable, unintelligibly obscure for anyone who doesn't have
bash-expansion intuitions, and is still something I'd use the tab
character to complete when typing.
Best wishes,
Norman
[1] ...for some value of 'primarily' which might not survive close
examination
--
Norman Gray : https://nxg.me.uk
--
You received this message because you are subscribed to the Google Groups "Racket
Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
