fetch all the links of files of a certain extension in a webpage.

filename_fetcher

// by default, it fetches pdf
// change pdf to an extension you want
var pdflinks = [];
Array.prototype.map.call(document.querySelectorAll("a[href$=\".pdf\"]"), function(e, i) {
  if ((pdflinks || []).indexOf(e.href) == -1) {
    pdflinks.push(e.href);
  }
});
console.log(pdflinks.join(" "));
// copy the logged file names
// and paste it to Terminal in this format: 'wget -i file1 file2 file3'