From 663c7647ea181b285fed35b549e740cab3c9e244 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 29 Feb 2024 17:39:11 +0100 Subject: [PATCH] update README --- time/README.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/time/README.md b/time/README.md index e2aec08..6b6cb06 100644 --- a/time/README.md +++ b/time/README.md @@ -6,6 +6,15 @@ Tiny package which interacts with the `C++` implementation concerning time. Require the package in your `lakefile.lean` and add `import Time` in your Lean file. +## Troubleshoot + +If you get an error that `c++` is not found, you can double-check with `which c++ g++ gcc` +and then install `gcc` with: + +``` +sudo apt install build-essential +``` + **Implemented Functions:** - `Time.getLocalTime` returns the local date/time as a `String`.