Use mktemp instead of $RANDOM to generate unique names
authorAndrea Canciani <ranma42@gmail.com>
Wed, 23 Apr 2014 09:37:25 +0000 (11:37 +0200)
committerAndrea Canciani <ranma42@gmail.com>
Wed, 23 Apr 2014 13:11:12 +0000 (15:11 +0200)
commit9b78ea6412e36e76a8eb05cd6dea9ecc31c8c2fc
tree230138fe4e2b6711ceb116b8881a1e47a9c3dff3
parentcad503aafd2c057c232f5da42ea4f4d94fdabbd2
Use mktemp instead of $RANDOM to generate unique names

Using $RANDOM is not safe because collisions can occur. An example of
such a failure is available here:
https://s3.amazonaws.com/archive.travis-ci.org/jobs/23572639/log.txt

Using mktemp avoids this issue and removes the dependency on bash.
mcs/class/monodoc/jay.sh