1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
#!/usr/bin/awk -f BEGIN{ srand() # seed by time srand(seed+srand()) # allow additional external seed } { lines[++d]=$0 } END{ while (d > 0) { if (e==d) {break} r = int(1 + rand() * d) print lines[r] lines[r] = lines[d] delete lines[d] --d } }