+\input texinfo @c -*- texinfo -*-
+@c %**start of header
+@setfilename projects.info
+@settitle Pintos Projects
+@c %**end of header
+
+@c @bibref{} macro
+@iftex
+@macro bibref{cite}
+[\cite\]
+@end macro
+@end iftex
+@ifinfo
+@ifnotplaintext
+@macro bibref{cite}
+@ref{\cite\}
+@end macro
+@end ifnotplaintext
+@ifplaintext
+@macro bibref{cite}
+[\cite\]
+@end macro
+@end ifplaintext
+@end ifinfo
+@ifhtml
+@macro bibref{cite}
+[@ref{\cite\}]
+@end macro
+@end ifhtml
+
+@titlepage
+@title Pintos Projects
+@end titlepage
+
+@contents
+
+@ifnottex