Remove redundant title
This commit is contained in:
parent
34f205c4da
commit
eabbae7e39
1 changed files with 0 additions and 2 deletions
|
@ -1,5 +1,3 @@
|
||||||
#+TITLE: :lang fstar
|
|
||||||
|
|
||||||
#+TITLE: lang/fstar
|
#+TITLE: lang/fstar
|
||||||
#+DATE: February 2, 2020
|
#+DATE: February 2, 2020
|
||||||
#+SINCE: 2.0.10
|
#+SINCE: 2.0.10
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue