the basics for client-side filtering + a few tweaks

[plewww.git] / planetlab / js / plc_paginate.js

diff --git a/planetlab/js/plc_paginate.js b/planetlab/js/plc_paginate.js
index fcfe00a..32b44a1 100644 (file)
--- a/planetlab/js/plc_paginate.js
+++ b/planetlab/js/plc_paginate.js
@@ -1,3 +1,5 @@
+/* $Id$ */
+
 function displayTextInfo (opts,tablename) {
 
   if(!("currentPage" in opts)) { return; }
@@ -13,3 +15,4 @@ function displayTextInfo (opts,tablename) {
   b.appendChild(p);
 }
 
+