git-instaweb: Remove pidfile after stopping web server

diff --git a/thread-utils.h b/thread-utils.h
index cce4b77bd6452e2ec589d8c0dc0e8156352dd67b..1727a03333b80f2a01ca029162a4b511480a86e8 100644 (file)
--- a/thread-utils.h
+++ b/thread-utils.h
@@ -2,5 +2,6 @@
 #define THREAD_COMPAT_H
 
 extern int online_cpus(void);
+extern int init_recursive_mutex(pthread_mutex_t*);
 
 #endif /* THREAD_COMPAT_H */