The `mkdir -p ` should take care of that if necessary, by creating the directory, but yeah, ideally, if it doesn't already exist on most Linux distros we should try and avoid creating a directory that is non-standard.
I'm reasonably indifferent on where the MANDIR defaults to, to be honest. My end goal is being able to set the MANDIR, so whatever works best for everyone else within that end goal I'm entirely happy with. Dom Sent from OS X. If you wish to communicate more securely my PGP Public Key is 0x872524db9d74326c. On 02/02/2015 12:41, Gabriel Kerneis wrote: > Le 2015-02-02 02:57, Juliusz Chroboczek a écrit : >>> +MANDIR = $(PREFIX)/share/man >> >> Dominyk, Gabriel, Julien, I'm tempted to make this $(PREFIX)/man by >> default. >> Objections? > > GNU defaults to $(DATAROOTDIR)/man, where $DATAROOTDIR defaults to > $(PREFIX)/share. Also, /usr/man does not exist on my Debian, whereas > /usr/share/man does; so your default would break for PREFIX=/usr. > I would stick with Dominyk's $(PREFIX)/share/man here. > > Best, _______________________________________________ Babel-users mailing list [email protected] http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/babel-users
