+int PushSearchPath (SearchPath* P, const char* NewPath);
+/* Add a new search path to the head of an existing search path list, provided
+ * that it's not already there. If the path is already at the first position,
+ * return zero, otherwise return a non zero value.
+ */
+
+void PopSearchPath (SearchPath* P);
+/* Remove a search path from the head of an existing search path list */
+
+void ForgetSearchPath (SearchPath* P);
+/* Forget all search paths in the given list */