I tried that, and that seemed to work, however the logic of say aliasing
tup to MYRANDOM=$RANDOM tup means that if someone clones the git repo
from scratch, and doesn't know about this, they won't have this
functionality.
The same problem is present with a git hook. If someone clones the repo
and doesn't apply the extra step to make things work, the build they
produce might not have the current hash.
/Matt
On 2014.05.20. 17:57, Lee Winter wrote:
On Fri, May 16, 2014 at 3:16 PM, Matthias Vegh <[email protected]
<mailto:[email protected]>> wrote:
I'm a colleague of the original poster, and have spent the
majority of today trying to get this work. It can be done, but
requires a gruesome hack.
My first attempt was to add an environment variable to the mix,
one that always changes, and would influence the rule that
generated the git hash. Seeing as various shells provide such a
variable-like thing ($RANDOM) I started there. It turns out, that
$RANDOM is not exactly an environment variable.
(I'm not sure how exactly, but tup couldn't export it).
Can you assign $RANDOM to MYRANDOM and export that?
Something about all programming problems can be simplified by the
addition of an extra level of indirection.
-- Lee
--
--
tup-users mailing list
email: [email protected]
unsubscribe: [email protected]
options: http://groups.google.com/group/tup-users?hl=en
---
You received this message because you are subscribed to a topic in the
Google Groups "tup-users" group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/tup-users/e_1ynmm1GA8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to
[email protected]
<mailto:[email protected]>.
For more options, visit https://groups.google.com/d/optout.
--
--
tup-users mailing list
email: [email protected]
unsubscribe: [email protected]
options: http://groups.google.com/group/tup-users?hl=en
---
You received this message because you are subscribed to the Google Groups "tup-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
For more options, visit https://groups.google.com/d/optout.
