Skip to main content

write_project_data

lean_ctx::core::pathjail_write

Function write_project_data 

Source 
pub fn write_project_data(
    project_root: &Path,
    rel: &Path,
    content: &[u8],
) -> Result<PathBuf, String>
Expand description

Write <project>/.lean-ctx/<rel>: the project root is trusted, .lean-ctx and everything below it must not be a symlink.