search.php

   1 <?php
   2 $path = ' '.escapeshellarg('*.html');
   3 $cmd = "git grep -li -- ".escapeshellarg($Page).$path;
   4 $cmd .= ' |sort -R |head -n 10'; # random selection
   5 exec($cmd, $results);
   6
   7 if (!$results) {
   8         $results = ['index.html'];
   9 }
  10
  11 require_once('nieuws.inc.php');
  12 print '<ul>';
  13 foreach ($results as $result) {
  14         $page = new ArchiveArticle($result);
  15         printf('<li><a href="/%s">%s</a></li>'."\n", $page->link, $page->name);
  16 }
  17 print "</ul>\n";