Skip to content

Followup for PR #2448#2682

Merged
mmhat merged 1 commit intodhall-lang:mainfrom
mmhat:maps-to-directory-tree-followup
Jan 31, 2026
Merged

Followup for PR #2448#2682
mmhat merged 1 commit intodhall-lang:mainfrom
mmhat:maps-to-directory-tree-followup

Conversation

@mmhat
Copy link
Collaborator

@mmhat mmhat commented Jan 31, 2026

This PR implements the changes discussed in PR #2448 (and implemented in nikita-volkov#1).

@mmhat mmhat force-pushed the maps-to-directory-tree-followup branch from 2d8b56b to d5f02fe Compare January 31, 2026 05:25
@mmhat mmhat enabled auto-merge (squash) January 31, 2026 05:26
 * Added `DirectoryTreeOptions` type that allows one to control the
   behaviout or to-directory-tree
 * Added command line flags for these options: --allow-parent-directory
   and --allow-absolute-paths
 * Simplified code a bit
@mmhat mmhat force-pushed the maps-to-directory-tree-followup branch from d5f02fe to ebb539e Compare January 31, 2026 06:00
@mmhat mmhat merged commit 4033854 into dhall-lang:main Jan 31, 2026
8 checks passed
@mmhat mmhat deleted the maps-to-directory-tree-followup branch January 31, 2026 06:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant