Estrarre righe a caso da un file

[Alberto Fornasier]

On Thu, 11 Dec 2003 12:32:48 +0000
Alberto Fornasier <gimli@email.it> wrote:

> Ciao a tutti.
> Avrei necessita' di estrarre n righe a caso, senza ripetizioni da un
> file di testo, ma non riesco a farlo.
> Pensavo di fare uno scriptino bash usando $RANDOM e sed, ma non riesco
> a dire a sed di stamparmi solo le righe che gli indico.
> Qualche idea?
> 

Never mind, risolto.

Ciao