diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp
index 23a585d11..fccc9ca11 100644
--- a/src/util/lean_path.cpp
+++ b/src/util/lean_path.cpp
@@ -267,4 +267,31 @@ void display_path(std::ostream & out, std::string const & fname) {
     out << fname;
 #endif
 }
+
+std::string dirname(char const * fname) {
+    if (fname == nullptr)
+        return ".";
+    unsigned i = 0;
+    optional<unsigned> last_sep;
+    char const * it = fname;
+    while (*it) {
+        if (*it == g_sep)
+            last_sep = i;
+        ++i;
+        ++it;
+    }
+    if (!last_sep)
+        return ".";
+    std::string r;
+    for (unsigned i = 0; i < *last_sep; i++)
+        r.push_back(fname[i]);
+    return r;
+}
+
+std::string path_append(char const * p1, char const * p2) {
+    std::string r(p1);
+    r += g_sep;
+    r += p2;
+    return r;
+}
 }
diff --git a/src/util/lean_path.h b/src/util/lean_path.h
index f41d257aa..ce47963aa 100644
--- a/src/util/lean_path.h
+++ b/src/util/lean_path.h
@@ -38,4 +38,7 @@ std::string name_to_file(name const & fname);
     In some platforms it will fix the notation used to display the path.
 */
 void display_path(std::ostream & out, std::string const & fname);
+
+std::string dirname(char const * fname);
+std::string path_append(char const * path1, char const * path2);
 }