diff options
| -rw-r--r-- | polly/www/menu.html.incl | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/polly/www/menu.html.incl b/polly/www/menu.html.incl index 8b53de3a71a..75db58549fc 100644 --- a/polly/www/menu.html.incl +++ b/polly/www/menu.html.incl @@ -45,26 +45,6 @@ Optimizations</span></h2> <a href="http://repo.or.cz/w/polly-mirror.git">Browse (GitWeb)</a> </div> - <div class="submenu2"> - <label><a href="http://polyhedral.info" style="color: white">polyhedral.info - News</a></label> - <script language="JavaScript" - src="http://feed2js.org//feed2js.php?src=http%3A%2F%2Fpolyhedral.info%2Frss.xml&num=5&date=y&utf=y&desc=200" - charset="UTF-8" type="text/javascript"></script> - - <noscript> - <a - href="http://feed2js.org//feed2js.php?src=http%3A%2F%2Fpolyhedral.info%2Frss.xml&num=5&date=y&utf=y&html=y">View - RSS feed</a> - </noscript> -<script src="http://code.jquery.com/jquery-latest.min.js" type="text/javascript"></script> -<script type='text/javascript'> -function myFormat(dateTime) { - var months = ['Jan','Feb','Mar','Apr','May','Jun','Jul','Aug','Sep','Oct','Nov','Dec']; - var dateString = months[dateTime.getMonth()] + ' ' + dateTime.getDate() + ', ' + dateTime.getFullYear(); - return dateString; -} -$(document).ready(function() {$('.rss-date').each(function() {$(this).text(myFormat(new Date($(this).text())));});}); -</script> </div> </div> |
