void jsextrarandom(char *seed);